proposition: Lemma d_CMetricSpace_apdiag_imp_grzero : forall X : CMetricSpace, apdiag_imp_grzero (cms_crr X) (cms_d (c:=X)).
proof: Proof. intro X. apply ax_d_apdiag_imp_grzero. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv