proposition: Lemma PlotPath_correct : eq PlotPath PlotPath_slow.
proof: Proof. unfold PlotPath, PlotPath_slow, RasterizeQ2. rewrite map_map. unfold CompactIntervalQ, approximate. unfold CompactIntervalQ_raw, UniformPartition. rewrite map_map. reflexivity. 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