fact: Definition CRball (r: CR) (x y: M): Prop := forall (q:Q), r <= ' q -> ball q x y.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs