proposition: Lemma HausdorffBallHausdorffBallStrong : forall (e:Q) (a b:FinEnum), ball e a b -> hausdorffBallStrong X e (fun x => InFinEnumC x a) (fun x => InFinEnumC x b).
proof: Proof. intros e a b [H0 H1]. split; apply HemiMetricHemiMetricStrong; apply H1. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength