proposition: Lemma hemiMetric_triangle : forall e0 e1 A B C, hemiMetric e0 A B -> hemiMetric e1 B C -> hemiMetric (e0 + e1) A C.
proof: Proof. intros e0 e1 A B C H0 H1 x Hx. destruct (H0 x Hx) as [HG | y [Hy Hxy]] using existsC_ind. apply existsC_stable; assumption. destruct (H1 y Hy) as [HG | z [Hz Hyz]] using existsC_ind. apply existsC_stable; assumption. apply existsWeaken. exists z. split; try assumption. apply ball_triangle with y; 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