proposition: Theorem pred_le_id : forall x, (pred x <= x)%R.
proof: Proof. intros x; unfold pred. pattern x at 2; rewrite <- (Ropp_involutive x). apply Ropp_le_contravar. apply succ_ge_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop