proposition: Lemma Fle2_spec : forall x y, Fle2_prop x y (Fle2 x y).
proof: Proof. intros x y. case_eq (Fle2 x y) ; intros H. apply Fle2_true. apply Fle2_correct. exact H. generalize H. clear H. unfold Fle2. case_eq (Fcomp2 x y) ; try (intros ; discriminate). intros H _. apply Fle2_false. apply Rcompare_Gt_inv. now rewrite <- Fcomp2_correct. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions