fact: Definition PlotPath : positive * positive * Q * sparse_raster n m := (n, m, 2, let num := (Z.to_pos (Qceiling ((to - from) / (inject_Z 2 * ((1 # 2) * ` (FinEnum_map_modulus (1 # 1)%Qpos (mu path) err)))))) in sparse_raster_data n m (map (λ x : Z, rasterize2 n m t l b r (let (a, b0) := approximate (path (AppInverse0 (from + (to - from) * (2 * x + 1 # 1) / (2 * Z.pos num # 1)) ((1 # 2)%Qpos * FinEnum_map_modulus (1#1)%Qpos (mu path) err)%Qpos)) err in (AQtoQ a, AQtoQ b0))) (Interval.iterateN_succ 0 num))).
imports: Coq.QArith.Qround CoRN.reals.fast.Plot CoRN.reals.faster.ARArith CoRN.reals.faster.ARinterval CoRN.model.metric2.Qmetric