proposition: Lemma plFEQ : PrelengthSpace (FinEnum Q_as_MetricSpace).
proof: Proof. apply FinEnum_prelength. apply locatedQ. apply QPrelengthSpace. Qed.
imports: QArith.Qround CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterizeQ CoRN.reals.fast.Interval CoRN.metric2.Graph CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax