proposition: Theorem succ_le : forall x y, F x -> F y -> (x <= y)%R -> (succ x <= succ y)%R.
proof: Proof. intros x y Fx Fy Hxy. apply Ropp_le_cancel. rewrite <- 2!pred_opp. apply pred_le. now apply generic_format_opp. now apply generic_format_opp. now apply Ropp_le_contravar. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop