proposition: Theorem FLXN_format_satisfies_any : satisfies_any FLXN_format.
proof: Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). split ; intros H. now apply FLXN_format_generic. now apply generic_format_FLXN. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE