proposition: Lemma CRopp_lt_cancel : forall x y : CR, -y < -x -> x < y.
proof: Proof. intros. apply (CRplus_lt_l _ _ (-x-y)). assert (-y == -x-y+x)%CR by ring. assert (-x == -x-y+y)%CR by ring. apply (CRltT_wd H0 H1), 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