proposition: Theorem Fcmp_correct : forall beta (x y : float beta), Fcmp x y = Xcmp (FtoX x) (FtoX y).
proof: Proof. intros. case x ; intros ; simpl ; try apply refl_equal ; case y ; intros ; simpl ; try apply refl_equal ; clear. now rewrite Rcompare_Eq. case b. rewrite Rcompare_Gt. apply refl_equal. apply FtoR_Rneg. rewrite Rcompare_Lt. apply refl_equal. apply FtoR_Rpos. now case b ; apply refl_equal. case b. rewrite Rcompare_Lt. apply refl_equal. apply FtoR_Rneg. rewrite Rcompare_Gt. apply refl_equal. apply FtoR_Rpos. case b ; case b0. rewrite Fcmp_aux2_correct. simpl. change true with (negb false). repeat rewrite <- FtoR_neg. generalize (FtoR beta false p0 z0). generalize (FtoR beta false p z). intros. destruct (Rcompare_spec r0 r). rewrite Rcompare_Lt. apply refl_equal. now apply Ropp_lt_contravar. rewrite H. now rewrite Rcompare_Eq. rewrite Rcompare_Gt. apply refl_equal. apply Ropp_lt_contravar. exact H. rewrite Rcompare_Lt. apply refl_equal. apply Rlt_trans with R0. apply FtoR_Rneg. apply FtoR_Rpos. rewrite Rcompare_Gt. apply refl_equal. apply Rlt_trans with R0. apply FtoR_Rneg. apply FtoR_Rpos. rewrite Fcmp_aux2_correct. apply refl_equal. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic