Lemma m_c0 c0 l : list_max (c0 :: l) <= c0 -> False.
Lemma max_value k l: In k l -> k <= list_max l. This lemma may be helpful in proving above?
You can prove
list_max (c0 :: l) < c0 -> False, but with
<= there are many counterexamples (take
l := ).
I think you would prove the
< version by showing
c0 <= list_max (c0 :: l) and then using some standard lemma to turn
max_value (or_introl eq_refl) should be enough.
Last updated: Jan 28 2023 at 07:30 UTC