proposition: Theorem generic_format_bpow : forall e, (fexp (e + 1) <= e)%Z -> generic_format (bpow e).
proof: Proof. intros e H. unfold generic_format, scaled_mantissa, cexp. rewrite mag_bpow. rewrite <- bpow_plus. rewrite <- (IZR_Zpower beta (e + - fexp (e + 1))). rewrite Ztrunc_IZR. rewrite <- F2R_bpow. rewrite F2R_change_exp with (1 := H). now rewrite Zmult_1_l. now apply Zle_minus_le_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop