proposition: Lemma CRplus_lt_r (x y z: CR): prod (x < y -> x+z < y+z) (x+z < y+z -> x < y).
proof: Proof. split. - intros. destruct H as [q H]. exists q. setoid_replace (y+z-(x+z))%CR with (y-x)%CR by (unfold equiv, msp_Equiv; ring). exact H. - intros. destruct H as [q H]. exists q. setoid_replace (y-x) with (y+z-(x+z)) by (unfold equiv, msp_Equiv; ring). exact H. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders