proposition: Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
proof: Proof. intros r r1 r2 H%(Rplus_lt_compat_l (-r)). now rewrite <-2Rplus_assoc, Rplus_opp_l, 2Rplus_0_l in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField