proposition: Theorem generic_format_FTZ : forall x, FTZ_format x -> generic_format beta FTZ_exp x.
proof: Proof. intros x Hx. cut (generic_format beta (FLX_exp prec) x). apply generic_inclusion_mag. intros Zx. destruct Hx as [[xm xe] Hx1 Hx2 Hx3]. simpl in Hx2, Hx3. specialize (Hx2 Zx). assert (Zxm: xm <> Z0). contradict Zx. rewrite Hx1, Zx. apply F2R_0. unfold FTZ_exp, FLX_exp. rewrite Zlt_bool_false. apply Z.le_refl. rewrite Hx1, mag_F2R with (1 := Zxm). cut (prec - 1 < mag beta (IZR xm))%Z. clear -Hx3 ; lia. apply mag_gt_Zpower with (1 := Zxm). apply Hx2. apply generic_format_FLXN. now apply FLXN_format_FTZ. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX