proposition: Theorem generic_format_FLT_1 : (emin <= 0)%Z -> generic_format beta FLT_exp 1.
proof: Proof. intros Hemin. now apply (generic_format_FLT_bpow 0). Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE