proposition: Lemma hausdorffBall_sym : forall e A B, hausdorffBall e A B -> hausdorffBall e B A.
proof: Proof. intros e A B [H0 H1]. split. exact H0. split; apply H1. Qed.
imports: CoRN.algebra.RSetoid CoRN.logic.Classic CoRN.metric2.Metric CoRN.metric2.Classification Coq.Lists.List Coq.ZArith.ZArith CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax