Stream: Coq users

Topic: Is contra statement?

sara lee (Dec 07 2021 at 16:34):

max b (list_max  l) <> 0 ->
 b <= list_max (b :: l) ->
 max b (list_max l) <= b -> False

Pierre Castéran (Dec 08 2021 at 09:27):

Hi, Sara,
It lacks some information about your statement, for instance about the variables land b (no quantifier nor hypothesis).
For instance, if I pose l := repeat 2 2and b:=2your statement is false.
Pierre

Last updated: Sep 26 2023 at 11:01 UTC