proposition: Theorem generic_format_pred : forall x, F x -> F (pred x).
proof: Proof. intros x Fx. unfold pred. apply generic_format_opp. apply generic_format_succ. now apply generic_format_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop