I have started working in Coq. I want to use list_max l function and show that all elements of list are less or equal to the value found by function ( list_max l ). What steps I should take?

It depends how you write the fact that an element belongs to the list. The idea would be to use `list_max_le`

with `n:=list_max l`

. This gives you a `Forall`

statement that you can turn into an `In`

statement by using `Forall_forall`

.

(deleted)

I want to write a recursive function which takes n different values from user and add them in the list. I have idea about fix value input argument but not varying values.

Last updated: Oct 04 2023 at 23:01 UTC