proposition: Lemma metric_ap_cotransitive : forall X : CPsMetricSpace, cotransitive (metric_ap X).
proof: Proof. intro X. unfold cotransitive in |- *. unfold metric_ap in |- *. intros x y H z. cut (ZeroR[<](x[-d]z)[+](z[-d]y)). intro H0. apply positive_Sum_two. exact H0. apply less_leEq_trans with (x[-d]y). exact H. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv