proposition: Theorem generic_format_bpow_inv : forall e, generic_format (bpow e) -> (fexp e <= e)%Z.
proof: Proof. intros e He. apply generic_format_bpow_inv' in He. assert (H := valid_exp_large' (e + 1) e). lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop