proposition: Lemma Rplus_le_compat : forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
proof: Proof. intros r1 r2 r3 r4 r1_lt_r2 r3_lt_r4; apply (Rle_trans _ (r2 + r3)). - now apply Rplus_le_compat_r. - now apply Rplus_le_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField