fact: Definition PlotPath_slow : positive * positive * Q * sparse_raster n m := (n, m, 2#1, sparse_raster_data n m (map (λ x : AQ_as_MetricSpace, rasterize2 n m t l b r (let (a, b0) := approximate (path x) err in (AQtoQ a, AQtoQ b0))) (approximate (IabCompact from to Hfromto) (FinEnum_map_modulus (1 # 1) (mu path) err)))).
imports: Coq.QArith.Qround CoRN.reals.fast.Plot CoRN.reals.faster.ARArith CoRN.reals.faster.ARinterval CoRN.model.metric2.Qmetric