proposition: Theorem generic_format_FIX_FLT : forall x : R, generic_format beta FLT_exp x -> generic_format beta (FIX_exp emin) x.
proof: Proof. clear prec_gt_0_. intros x Hx. rewrite Hx. apply generic_format_F2R. intros _. rewrite <- Hx. apply Z.le_max_r. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE