proposition: Lemma located_imp_located' : forall (X : CPsMetricSpace) (P : X -> CProp), located P -> located' P.
proof: Proof. intros X P. unfold located in |- *. unfold located' in |- *. intros H x y. set (H0 := H x y) in *. elim H0. intros x0 H1. exists x0. unfold dsub' in H1. generalize H1. unfold dsub'_as_cs_fun in |- *. unfold dsub' in |- *. simpl in |- *. unfold set_glb_IR in |- *. intros. split. intro x1. elim H2. intros a b H3. apply a. elim H3. intros. exists x2. astepl (x[-d]from_SubPsMetricSpace X P x2). exact p. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. intros e H3. elim H2. intros. set (H8 := b e H3) in *. elim H8. intros. exists x1. elim p. intros. exists x2. astepl (from_SubPsMetricSpace X P x2[-d]x). exact p0. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. exact q. Qed.
imports: CoRN.metrics.Prod_Sub