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.
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
nth_In, you can infer
nth k (c :: l) 0 <= c from your hypotheses. Then your proof is completed with
May be you should write the proof on paper before writing the formal proof script.
Last updated: Jan 27 2023 at 02:04 UTC