proposition: Lemma mspc_ball_wd : forall (e d : Qinf) x1 x2 y1 y2, e = d -> x1 = x2 -> y1 = y2 -> (mspc_ball e x1 y1 <-> mspc_ball d x2 y2).
proof: Proof. unfold equiv, mspc_equiv. split. - intros. destruct d as [d|]. 2: apply mspc_ball_inf. destruct e as [e|]. 2: inversion H1. simpl in H1. assert (0+(e+0) == d). { rewrite Qplus_0_r, Qplus_0_l. exact H1. } apply (mspc_ball_e_wd _ _ x2 y2 H5). clear H5 H1 d. pose proof (mspc_triangle 0 (e+0) x2 x1 y2). apply H1. clear H1. apply mspc_sym, H2. pose proof (mspc_triangle e 0 x1 y1 y2). apply H5. exact H4. exact H3. - intros. destruct e as [e|]. 2: apply mspc_ball_inf. destruct d as [d|]. 2: inversion H1. simpl in H1. assert (0+(d+0) == e). { rewrite Qplus_0_r, Qplus_0_l. rewrite H1. reflexivity. } apply (mspc_ball_e_wd _ _ x1 y1 H5). clear H5 H1 e. pose proof (mspc_triangle 0 (d+0) x1 x2 y1). apply H1. exact H2. clear H1. pose proof (mspc_triangle d 0 x2 y2 y1). apply H1. exact H4. apply mspc_sym, H3. 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