proposition: Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
proof: Proof. intros r r1 r2 [Ilt | Eq]. - left; apply (Rplus_lt_reg_l r r1 r2 Ilt). - right; apply (Rplus_eq_reg_l r r1 r2 Eq). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField