proposition: Theorem Rplus_lt_mono : forall n m p q : R, n < m -> p < q -> n + p < m + q.
proof: Proof. intros n m p q H1 H2. apply Rlt_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_lt_mono_l]. Qed.
imports: Setoid Ring