proposition: Lemma AQball_abs (ε : Q) (x y : AQ_as_MetricSpace) : ball ε x y ↔ 'abs (x - y) ≤ ε.
proof: Proof. simpl. rewrite Qball_Qabs. now rewrite abs.preserves_abs, rings.preserves_minus. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring CoRN.util.Qdlog CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.metric2.MetricMorphisms CoRN.reals.faster.ApproximateRationals