proposition: Lemma FinSubset_ball_nil : forall e x, ~FinSubset_ball e x nil.
proof: Proof. intros e x H. unfold FinSubset_ball in H. contradict H; intros [y [H _]]. contradiction. 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