proposition: Lemma gball_CRabs (r : Q) (x y : CR) : ball r x y <-> CRabs (x - y) <= ' r.
proof: Proof. rewrite rational. apply as_distance_bound. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs