proposition: Lemma FinEnum_ball_e_wd : forall (e1 e2:Q) (a b : list X), (e1 == e2) -> (FinEnum_ball e1 a b <-> FinEnum_ball e2 a b).
proof: Proof. intros e1 e2 a b He. apply hausdorffBall_wd; auto with *. 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