Commit 54f0afbe authored by MARCHE Claude's avatar MARCHE Claude

more lemmas for full model of floats

parent ba6fd292
......@@ -544,7 +544,6 @@ theory GenFloatSpecFull
lemma lt_le_trans:
forall x y z:t. lt x y /\ le y z -> lt x z
(*
lemma le_ge_asym:
forall x y:t. le x y /\ ge x y -> eq x y
......@@ -553,7 +552,6 @@ theory GenFloatSpecFull
lemma not_gt_le: forall x y:t.
not (gt x y) /\ is_not_NaN x /\ is_not_NaN y -> le x y
*)
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment