proposition: Lemma Metric_d_apdiag_grzero : forall X : CPsMetricSpace, apdiag_imp_grzero (QuotientCPsMetricSpace X) (cms_d (c:=QuotientCPsMetricSpace X)).
proof: Proof. intro X. unfold apdiag_imp_grzero in |- *. intros x y. simpl in |- *. unfold metric_ap in |- *. unfold metric_d in |- *. intuition. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv