proposition: Lemma CRdistance_CRle (r x y: CR): x - r <= y /\ y <= x + r <-> CRdistance x y <= r.
proof: Proof. intros. unfold CRdistance. rewrite CRabs_AbsSmall. simpl. rewrite (CRplus_le_l (x - r) y (r - y)). CRring_replace (r - y + (x - r)) (x - y). CRring_replace (r - y + y) r. rewrite (CRplus_le_l y (x + r) (-r - y)). CRring_replace (-r - y + y) (-r). CRring_replace (- r - y + (x + r)) (x - y). intuition. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Stability