What next command I should apply ?

```
Lemma max_greater : forall m h l, In m (h :: l) ->
m <= list_max (h :: l).
Proof.
intros.
apply (Forall_forall (fun k : nat => k <= (list_max (h::l))) l).
apply (list_max_le l (list_max (h::l))). simpl in H.
```

First goal will be OK but not the second one.

You should probably use `apply (Forall_forall (fun k : nat => k <= (list_max (h::l))) (h::l)).`

in the second line of your proof.

Thank you.

```
c k: nat l : list nat
H : k < length (c :: l)
H1 : list_max (c :: l) <= c
Goal: nth k (c :: l) 0 > c -> False
```

In want to write goal statement in term of list_max (c :: l) ,is it possible?

With three lemmas of the `List`

library: `list_max_le`

, `Forall_forall`

and `nth_In`

, you can infer `nth k (c :: l) 0 <= c`

from your hypotheses. Then your proof is completed with `lia`

.

May be you should write the proof on paper before writing the formal proof script.

Last updated: Jun 15 2024 at 09:01 UTC