proposition: Lemma in_CRball (r: Q) (x y : CR) : x - ' r <= y /\ y <= x + ' r <-> ball r x y.
proof: Proof. Proof with intuition. intros. cut ((-' r <= x - y /\ x-y <= 'r) <-> (x - ' r <= y /\ y <= x + ' r)). - pose proof (CRAbsSmall_ball x y r)... - simpl. setoid_replace (x - y <= ' r) with (x - ' r <= y). setoid_replace (- ' r <= x - y) with (y <= x + ' r). intuition. rewrite (CRplus_le_r (- ' r) (x - y) ('r + y)). assert (- ' r + (' r + y) == y) as E by ring. rewrite E. assert (x - y + (' r + y) == x + ' r)%CR as F by ring. rewrite F... rewrite (CRplus_le_r (x - y) (' r) (y - 'r)). assert (x - y + (y - ' r) == x - ' r) as E by ring. rewrite E. assert (' r + (y - ' r) == y) as F by ring. rewrite F... 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