proposition: Theorem FLXN_format_FTZ : forall x, FTZ_format x -> FLXN_format beta prec x.
proof: Proof. intros x [[xm xe] Hx1 Hx2 Hx3]. eexists. exact Hx1. exact Hx2. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX