Classification of metric spaces

There is a heirarchy of properties that a metric space can possess. At the lowest level a metric space is stable if its ball relation is double negation stable. Arguablely this could be made a requirement of metric spaces.
Definition stableMetric (ms:MetricSpace) :=
 forall e (x y:ms), ~~(ball e x y) -> ball e x y.

Lemma stableEq : forall (ms:MetricSpace) (stable:stableMetric ms) (x y:ms),
 ~~(st_eq x y) -> st_eq x y.

At the next level up a metric space is located if you can choose between ball d x y and ~ball e x y for e < d. Every located metric is a stable metric.
Definition locatedMetric (ms:MetricSpace) :=
 forall (e d:Qpos) (x y:ms), e < d -> {ball d x y}+{~ball e x y}.

At the top level a metric space is decidable if its ball relation is decidable. Every decidable metric is a located metric.
Definition decidableMetric (ms:MetricSpace) :=
 forall e (x y:ms), {ball e x y}+{~ball e x y}.

Lemma decidable_located : forall ms,
 decidableMetric ms -> locatedMetric ms.

Lemma located_stable : forall ms,
 locatedMetric ms -> stableMetric ms.