proposition: Lemma FinSubset_ball_app_orC : forall e x l1 l2, FinSubset_ball e x (l1 ++ l2) -> orC (FinSubset_ball e x l1) (FinSubset_ball e x l2).
proof: Proof. intros e x l1 l2 H [H0 H1]. unfold FinSubset_ball in H. contradict H; intros [y [H H2]]. apply in_app_iff in H. destruct H. contradict H0. intro abs. contradict abs. exists y. split; assumption. contradict H1. 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