proposition: Lemma mspc_eq a b: (∀ e: Qpos, mspc_ball e a b) → a = b.
proof: Proof. Proof with auto. intros. apply mspc_closed. intros. rewrite (mspc_ball_proper (0+d)%Qinf d). apply H1. change (0 + d == d). ring. 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