proposition: Theorem bpow_le_F2R : forall m e : Z, (0 < m)%Z -> (bpow e <= F2R (Float beta m e))%R.
proof: Proof. intros m e H. rewrite <- F2R_bpow. apply F2R_le. now apply (Zlt_le_succ 0). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits