proposition: Theorem FLT_format_generic : forall x, generic_format beta FLT_exp x -> FLT_format x.
proof: Proof. intros x. unfold generic_format. set (ex := cexp beta FLT_exp x). set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)). intros Hx. rewrite Hx. eexists ; repeat split ; simpl. apply lt_IZR. rewrite IZR_Zpower. 2: now apply Zlt_le_weak. apply Rmult_lt_reg_r with (bpow ex). apply bpow_gt_0. rewrite <- bpow_plus. change (F2R (Float beta (Z.abs mx) ex) < bpow (prec + ex))%R. rewrite F2R_Zabs. rewrite <- Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0, Rabs_R0. apply bpow_gt_0. unfold cexp in ex. destruct (mag beta x) as (ex', He). simpl in ex. specialize (He Hx0). apply Rlt_le_trans with (1 := proj2 He). apply bpow_le. cut (ex' - prec <= ex)%Z. lia. unfold ex, FLT_exp. apply Z.le_max_l. 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