proposition: Lemma Rplus_npos_le : forall r1 r2, r2 <= 0 -> r1 + r2 <= r1.
proof: Proof. now intros r1 r2 H; rewrite <-(Rplus_0_r r1) at 2; apply Rplus_le_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField