proposition: Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.
proof: Proof. intros r r1 r2 H. rewrite (Rplus_comm r1), (Rplus_comm r2) in H. now apply (Rplus_lt_reg_l r). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField