Commit 28a6cacc authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

Fle0 is transitive

parent a4567d95
......@@ -98,4 +98,28 @@ Proof.
fdestruct x; fdestruct y.
Qed.
(**
[Fle0] is transitive
*)
Lemma Fle0_trans:
forall (x y z : float),
Fle0 x y = true -> Fle0 y z = true -> Fle0 x z = true.
Proof.
intros.
fdestruct y.
- fdestruct x; fdestruct z.
now destruct s, s0.
- fdestruct x; fdestruct z.
now destruct s, s0.
- fdestruct x; fdestruct z.
- fdestruct x; fdestruct z.
- fdestruct x; fdestruct z; simpl in *.
+ now destruct s, s0.
+ now destruct s.
+ now destruct s, s0.
+ now destruct s, s0.
+ now destruct s, s0.
+ apply (Bleb_trans _ _ _ H H0).
Qed.
End Fle0.
\ No newline at end of file
Supports Markdown
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