proposition: Theorem FLT_format_bpow : forall e, (emin <= e)%Z -> FLT_format (bpow e).
proof: Proof. intros e He. apply FLT_format_generic. now apply generic_format_FLT_bpow. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE