proposition: Lemma CRplus_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), r1 < r2 -> r1 + r < r2 + r.
proof: Proof. intros. destruct (CRisRing R). apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _) (CRplus R r2 r) (CRplus R r2 r)). - apply CReq_refl. - apply (CRlt_proper R _ _ (CReq_refl _) _ (CRplus R r r2)). + apply Radd_comm. + apply CRplus_lt_compat_l. exact H. Qed.
imports: QArith Qabs Qround