proposition: Lemma decidable_located : forall ms, decidableMetric ms -> locatedMetric ms.
proof: Proof. intros ms H e d x y Hed. destruct (H e x y). left. abstract ( apply ball_weak_le with e; try assumption; apply Qlt_le_weak; assumption). right; assumption. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric