proposition: Lemma PlotPath_correct : eq PlotPath PlotPath_slow.
proof: Proof. unfold PlotPath_slow. unfold IabCompact, approximate. rewrite map_map. unfold Interval.UniformPartition. rewrite map_map. reflexivity. Qed.
imports: Coq.QArith.Qround CoRN.reals.fast.Plot CoRN.reals.faster.ARArith CoRN.reals.faster.ARinterval CoRN.model.metric2.Qmetric