proposition: Lemma d_zero_imp_eq : forall (X : CMetricSpace) (a b : X), a[-d]b[=][0] -> a[=]b.
proof: Proof. intros X a b. intro H. apply not_ap_imp_eq. red in |- *. intro H1. generalize H. apply ap_imp_neq. apply Greater_imp_ap. apply ax_d_apdiag_imp_grzero. exact H1. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv