proposition: Lemma FinSubset_ball_app_l : forall e x l1 l2, FinSubset_ball e x l1 -> FinSubset_ball e x (l1 ++ l2).
proof: Proof. intros e x l1 l2 H abs. unfold FinSubset_ball in H. contradict H; intros [y H]. contradict abs. exists y. split. apply in_app_iff. left. apply H. apply H. 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