fact: Definition Metric_CSet_is_CSetoid (X : CPsMetricSpace) := Build_is_CSetoid X (metric_eq X) (metric_ap X) (metric_ap_irreflexive X) (metric_ap_symmetric X) (metric_ap_cotransitive X) ( metric_ap_tight X).
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv