proposition: Theorem le_F2R : forall e m1 m2 : Z, (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R -> (m1 <= m2)%Z.
proof: Proof. intros e m1 m2 H. apply le_IZR. apply Rmult_le_reg_r with (bpow e). apply bpow_gt_0. exact H. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits