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

Fle0 module

parent 82e06000
......@@ -8,5 +8,5 @@
./thry/Utils.v
./thry/B32.v
./thry/Correction_thms.v
./thry/Test.v
./thry/Fle0.v
./extraction.v
\ No newline at end of file
......@@ -88,4 +88,14 @@ Proof.
now destruct s.
Qed.
(**
[Fle0] is included in [Bleb].
*)
Lemma Fle0_Bleb:
forall (x y : float),
Fle0 x y = true -> Bleb x y = true.
Proof.
fdestruct x; fdestruct y.
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