(* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
-lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.x#y → 0 < δ x y.
+lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
intros 2 (R m); cases m 0; simplify; intros; assumption; qed.