proposition: Theorem generic_format_satisfies_any : satisfies_any generic_format.
proof: Proof. split. exact generic_format_0. exact generic_format_opp. intros x. eexists. apply round_DN_pt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop