proposition: Lemma hemiMetric_wd1 : forall (e0 e1:Q) A B, (e0 == e1) -> hemiMetric e0 A B -> hemiMetric e1 A B.
proof: Proof. intros e0 e1 A B He H x Hx. destruct (H x Hx) as [HG | y [Hy Hxy]] using existsC_ind. apply existsC_stable; assumption. apply existsWeaken. exists y. split. exact Hy. unfold QposEq in He. rewrite -> He in Hxy; auto. 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