proposition: Theorem pred_succ : forall x, F x -> pred (succ x) = x.
proof: Proof. intros x Fx. rewrite <- (Ropp_involutive x). rewrite succ_opp, pred_opp. apply f_equal, succ_pred. now apply generic_format_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop