proposition: Lemma hausdorffBall_wd1 : forall (e0 e1:Q) A B, (e0 == e1) -> hausdorffBall e0 A B -> hausdorffBall e1 A B.
proof: Proof. intros e0 e1 A B He [H0 H1]. split. rewrite <- He. exact H0. split; apply hemiMetric_wd1 with e0. exact He. apply H1. exact He. 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