proposition: Lemma hausdorffBallStrong_wd1 : forall (e0 e1:Q) A B, (e0 == e1) -> hausdorffBallStrong e0 A B -> hausdorffBallStrong e1 A B.
proof: Proof. intros e0 e1 A B He [H0 H1]. split; apply hemiMetricStrong_wd1 with e0; assumption. 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