proposition: Theorem Rcompare_F2R : forall e m1 m2 : Z, Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Z.compare m1 m2.
proof: Proof. intros e m1 m2. unfold F2R. simpl. rewrite Rcompare_mult_r. apply Rcompare_IZR. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits