proposition: Lemma in_Qball (r: Q) (x y: Q) : (x - r <= y <= x + r) <-> Qball r x y.
proof: Proof. now rewrite Qball_Qabs, Q.Qabs_diff_Qle. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals