proposition: Theorem generic_format_FLXN : forall x, FLXN_format x -> generic_format beta FLX_exp x.
proof: Proof. intros x [[xm ex] H1 H2]. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx. apply generic_format_0. specialize (H2 Zx). apply generic_format_FLX. rewrite H1. eexists ; repeat split. apply H2. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE