proposition: Lemma FinSubset_ball_wd : forall x y d e l, d == e -> msp_eq x y -> (FinSubset_ball d x l <-> FinSubset_ball e y l).
proof: Proof. split. - intros H1 abs. unfold FinSubset_ball in H1. contradict H1; intros [z [H1 H2]]. contradict abs. exists z. split. exact H1. rewrite <- H, <- H0. exact H2. - intros H1 abs. unfold FinSubset_ball in H1. contradict H1; intros [z [H1 H2]]. contradict abs. exists z. split. exact H1. rewrite H, H0. exact H2. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength