proposition: Lemma Fcomp2_correct : forall x y : float2, Fcomp2 x y = Rcompare x y.
proof: Proof. intros x y. unfold Fcomp2. generalize (Fshift2_correct x y). destruct (Fshift2 x y) as ((mx, my), e). intros (Hx, Hy). rewrite <- Hx, <- Hy. unfold float2R, F2R. simpl. rewrite Rcompare_mult_r. now rewrite Rcompare_IZR. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions