proposition: Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
proof: Proof. unfold Rle; intros r r1 r2 [Hlt | ->]. - now left; apply Rplus_lt_compat_l. - now right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField