proposition: Lemma FinSubset_ball_orC : forall e x a l, FinSubset_ball e x (a :: l) -> orC (ball e x a) (FinSubset_ball e x l).
proof: Proof. intros. intro abs. unfold FinSubset_ball in H. contradict H; intros [y [H H0]]. destruct H. - subst y. destruct abs. contradiction. - destruct abs. contradict H2. intro abs; contradict abs. exists y. split; assumption. 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