proposition: Lemma mspc_ball_Qabs (r x y : Q) : @ball _ (msp_mspc_ball Q_as_MetricSpace) r x y ↔ abs (x - y) ≤ r.
proof: Proof. apply gball_Qabs. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.metric2.Metric CoRN.ode.metric CoRN.model.totalorder.QposMinMax MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.orders.orders MathClasses.orders.semirings MathClasses.orders.rings MathClasses.theory.rings CoRN.model.metric2.CRmetric CoRN.model.setoids.Qsetoid CoRN.model.metric2.Qmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRball CoRN.reals.fast.CRabs MathClasses.theory.abs MathClasses.orders.minmax