proposition: Lemma d_wd : forall (X : CPsMetricSpace) (a b c : X), a[=]b -> a[-d]c[=]b[-d]c.
proof: Proof. intros X a b c. intros H. apply not_ap_imp_eq. red in |- *. intro H1. cut (a[#]b or c[#]c). intro H2. elim H2. apply eq_imp_not_ap. exact H. apply ap_irreflexive_unfolded. cut (a[-d]c[#]b[-d]c -> a[#]b or c[#]c). intro H2. apply H2. exact H1. apply csbf_strext. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv