proposition: Theorem FTZ_format_FLXN : forall x : R, (bpow (emin + prec - 1) <= Rabs x)%R -> FLXN_format beta prec x -> FTZ_format x.
proof: Proof. intros x Hx Fx. apply FTZ_format_generic. apply generic_format_FLXN in Fx. revert Hx Fx. apply generic_inclusion_ge. intros e He. unfold FTZ_exp. rewrite Zlt_bool_false. apply Z.le_refl. lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX