proposition: Lemma Feq2_correct : forall x y : float2, Feq2 x y = true -> x = y :>R.
proof: Proof. intros x y Hb. apply Rcompare_Eq_inv. rewrite <- Fcomp2_correct. revert Hb. unfold Feq2. now case Fcomp2. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions