proposition: Lemma FinSubset_ball_cons : forall x e a l, FinSubset_ball e x l -> FinSubset_ball e x (a :: l).
proof: Proof. intros. intro abs. unfold FinSubset_ball in H. contradict H; intros [z [H0 H1]]. contradict abs. exists z. split. right. exact H0. exact H1. 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