proposition: Theorem FLT_format_satisfies_any : satisfies_any FLT_format.
proof: Proof. refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)). intros x. split. apply FLT_format_generic. apply generic_format_FLT. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE