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