proposition: Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
proof: Proof. intros r r1 r2 r1_lt_r2; rewrite (Rplus_comm r1), (Rplus_comm r2). now apply Rplus_lt_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField