proposition: Lemma CRplus_le_lt_compat : forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R), r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
proof: Proof. intros. apply (CRle_lt_trans _ (CRplus R r2 r3)). - apply CRplus_le_compat_r. exact H. - apply CRplus_lt_compat_l. exact H0. Qed.
imports: QArith Qabs Qround