proposition: Lemma Qmetric_dec : decidableMetric Q_as_MetricSpace.
proof: Proof. intros e a b. simpl. simpl. unfold Qball, QAbsSmall. set (c:=-e). set (d:=(a-b)). destruct (Qlt_le_dec_fast d c) as [Hdc|Hdc]. right. abstract( intros [H1 H2]; apply (Qlt_not_le _ _ Hdc H1) ). destruct (Qlt_le_dec_fast e d) as [Hed|Hed]. right. abstract( intros [H1 H2]; apply (Qlt_not_le _ _ Hed H2) ). left. abstract auto. Defined.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals