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