proposition: Theorem generic_format_FLT : forall x, FLT_format x -> generic_format beta FLT_exp x.
proof: Proof. clear prec_gt_0_. intros x [[mx ex] H1 H2 H3]. simpl in H2, H3. rewrite H1. apply generic_format_F2R. intros Zmx. unfold cexp, FLT_exp. rewrite mag_F2R with (1 := Zmx). apply Z.max_lub with (2 := H3). 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 FLX FIX Ulp Round_NE