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