proposition: Theorem generic_format_ge_bpow : forall emin, ( forall e, (emin <= fexp e)%Z ) -> forall x, (0 < x)%R -> generic_format x -> (bpow emin <= x)%R.
proof: Proof. intros emin Emin x Hx Fx. rewrite Fx. apply Rle_trans with (bpow (fexp (mag beta x))). now apply bpow_le. apply bpow_le_F2R. apply gt_0_F2R with beta (cexp x). now rewrite <- Fx. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop