Definition Qball (e : Q+) (a b : Q) := AbsSmall (e:Q) (a - b).
Lemma Qball_Qabs : forall e a b, Qball e a b <-> Qabs (a - b) <= e.
Lemma Qle_closed : (forall e x, (forall d : Q+, x <= e+d) -> x <= e).
Notation QS := Q_is_Setoid (only parsing).
Lemma Q_is_MetricSpace : is_MetricSpace QS Qball.
Definition Q_as_MetricSpace : MetricSpace :=
@Build_MetricSpace QS _ Qball_wd Q_is_MetricSpace.
Lemma QPrelengthSpace_help : forall (e d1 d2:Qpos), e < d1+d2 -> forall (a b c:QS), ball e a b -> (c == (a*d2 + b*d1)/(d1+d2)%Qpos) -> ball d1 a c.
Q is a prelength space
Q is a decideable metric, and hence located and stable.
Lemma Qmetric_dec : decidableMetric Q_as_MetricSpace.
Lemma locatedQ : locatedMetric Q_as_MetricSpace.
Lemma stableQ : stableMetric Q_as_MetricSpace.
Lemma locatedQ : locatedMetric Q_as_MetricSpace.
Lemma stableQ : stableMetric Q_as_MetricSpace.