proposition: Lemma hemiMetricStrong_triangle : forall e0 e1 A B C, hemiMetricStrong e0 A B -> hemiMetricStrong e1 B C -> hemiMetricStrong (e0 + e1) A C.
proof: Proof. intros e0 e1 A B C H0 H1 x Hx d. assert (0 < (1#2)) as halfPos. reflexivity. destruct (H0 x Hx (exist _ _ halfPos*d)%Qpos) as [y [Hy Hxy]]. destruct (H1 y Hy (exist _ _ halfPos*d)%Qpos) as [z [Hz Hyz]]. exists z. split; try assumption. setoid_replace (e0 + e1 + proj1_sig d) with ((e0 + (1#2) * proj1_sig d) +(e1 + (1#2) * proj1_sig d))%Q by (simpl; ring). 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