proposition: Theorem generic_format_bpow_inv' : forall e, generic_format (bpow e) -> (fexp (e + 1) <= e)%Z.
proof: Proof. intros e He. apply Znot_gt_le. contradict He. unfold generic_format, scaled_mantissa, cexp, F2R. simpl. rewrite mag_bpow, <- bpow_plus. apply Rgt_not_eq. rewrite Ztrunc_floor. 2: apply bpow_ge_0. rewrite Zfloor_imp with (n := Z0). rewrite Rmult_0_l. apply bpow_gt_0. split. apply bpow_ge_0. apply (bpow_lt _ _ 0). clear -He ; lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop