proposition: Lemma hausdorffBallStrong_triangle : forall e0 e1 A B C, hausdorffBallStrong e0 A B -> hausdorffBallStrong e1 B C -> hausdorffBallStrong (e0 + e1) A C.
proof: Proof. intros e0 e1 A B C [H0A H0B] [H1A H1B]. split. apply hemiMetricStrong_triangle with B; assumption. apply hemiMetricStrong_wd1 with (e1 + e0)%Q. unfold QposEq. simpl. ring. apply hemiMetricStrong_triangle with B; 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