proposition: Theorem generic_format_FLX_FLT : forall x : R, generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
proof: Proof. clear prec_gt_0_. intros x Hx. unfold generic_format in Hx; rewrite Hx. apply generic_format_F2R. intros _. rewrite <- Hx. unfold cexp, FLX_exp, FLT_exp. apply Z.le_max_l. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE