proposition: Theorem generic_format_FLT_bpow : forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
proof: Proof. intros e He. apply generic_format_bpow; unfold FLT_exp. apply Z.max_case; try assumption. unfold Prec_gt_0 in prec_gt_0_; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE