proposition: Theorem F2R_lt : forall e m1 m2 : Z, (m1 < m2)%Z -> (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.
proof: Proof. intros e m1 m2 H. unfold F2R. simpl. apply Rmult_lt_compat_r. apply bpow_gt_0. now apply IZR_lt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits