proposition: Lemma Fle2_correct : forall x y : float2, Fle2 x y = true -> (x <= y)%R.
proof: Proof. intros x y Hb. apply Rcompare_not_Gt_inv. rewrite <- Fcomp2_correct. intros H. unfold Fle2 in Hb. now rewrite H in Hb. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions