```
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 `<=`

into `>`

. Indeed, `max_value (or_introl eq_refl)`

should be enough.

Last updated: Jan 28 2023 at 07:30 UTC