proposition: Lemma Metric_d_tri_ineq : forall X : CPsMetricSpace, tri_ineq (Metric_d X).
proof: Proof. intro X. unfold tri_ineq in |- *. intros x y z. unfold Metric_d in |- *. simpl in |- *. unfold metric_d in |- *. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv