Stream: Coq users

Topic: Is contra statement?


view this post on Zulip 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

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC