proposition: Lemma hemiMetricStrong_wd1 : forall (e0 e1:Q) A B, (e0 == e1) -> hemiMetricStrong e0 A B -> hemiMetricStrong e1 A B.
proof: Proof. intros e0 e1 A B He H x Hx d. destruct (H x Hx d) as [y [Hy Hxy]]. exists y. split. exact Hy. rewrite <- He. exact Hxy. 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