proposition: Lemma mspc_ball_e_wd : ∀ (e d : Q) (x y : X), e == d → mspc_ball e x y ↔ mspc_ball d x y.
proof: Proof. intros. apply mspc_ball_proper, H1. Qed.
imports: CoRN.algebra.RSetoid Arith List CoRN.model.totalorder.QposMinMax CSetoids Qmetric Qring Qinf QnnInf QnonNeg ProductMetric QposInf Qposclasses UniformContinuity MathClasses.implementations.stdlib_rationals stdlib_omissions.Pair stdlib_omissions.Q PointFree MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.theory.products