proposition: Theorem generic_format_FLX : forall x, FLX_format x -> generic_format beta FLX_exp x.
proof: Proof. clear prec_gt_0_. intros x [[mx ex] H1 H2]. simpl in H2. rewrite H1. apply generic_format_F2R. intros Zmx. unfold cexp, FLX_exp. rewrite mag_F2R with (1 := Zmx). apply Zplus_le_reg_r with (prec - ex)%Z. ring_simplify. now apply mag_le_Zpower. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE