proposition: Lemma CRplus_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), r1 + r < r2 + r -> r1 < r2.
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)) in H. 2: apply CReq_refl. apply (CRlt_proper R _ _ (CReq_refl _) _ (CRplus R r r2)) in H. - apply CRplus_lt_reg_l in H. exact H. - apply Radd_comm. Qed.
imports: QArith Qabs Qround