proposition: Lemma CRplus_lt_le_compat : forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R), r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4.
proof: Proof. intros. apply (CRlt_le_trans _ (CRplus R r2 r3)). - apply CRplus_lt_compat_r. exact H. - intro abs. apply CRplus_lt_reg_l in abs. contradiction. Qed.
imports: QArith Qabs Qround