proposition: Lemma Proper_uc_ball : Proper equiv mspc_ball.
proof: Proof. intros d e deeq f g fgeq h k hkeq. split. - intros [dpos H3]. split. rewrite <- deeq. exact dpos. intro x. specialize (H3 x). specialize (fgeq x). specialize (hkeq x). rewrite <- (@mspc_ball_wd B _ H2 d e (f x) (g x) (h x) (k x) deeq fgeq hkeq). exact H3. - intros [dpos H3]. split. rewrite deeq. exact dpos. intro x. specialize (H3 x). specialize (fgeq x). specialize (hkeq x). symmetry in deeq. apply mspc_sym in fgeq. apply mspc_sym in hkeq. rewrite <- (@mspc_ball_wd B _ H2 e d (g x) (f x) (k x) (h x) deeq fgeq hkeq). exact H3. exact H2. exact H2. 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 util.Container