proposition: Lemma hausdorffBall_triangle : forall e0 e1 A B C, hausdorffBall e0 A B -> hausdorffBall e1 B C -> hausdorffBall (e0 + e1) A C.
proof: Proof. intros e0 e1 A B C [H0A H0B] [H1A H1B]. split. apply (Qle_trans _ (e0 + 0)). rewrite Qplus_0_r. exact H0A. apply Qplus_le_r. exact H1A. split. apply hemiMetric_triangle with B. apply H0B. apply H1B. apply hemiMetric_wd1 with (e1 + e0)%Q. ring. apply hemiMetric_triangle with B. apply H1B. apply H0B. 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