proposition: Lemma Metric_d_pos_imp_ap : forall X : CPsMetricSpace, pos_imp_ap (Metric_d X).
proof: Proof. intro X. unfold pos_imp_ap in |- *. intros x y. unfold Metric_d in |- *. simpl in |- *. unfold metric_d in |- *. unfold metric_ap in |- *. intuition. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv