fact: Definition PixelizeQ2 {columns lines:positive} (points:sparse_raster columns lines) : raster columns lines := fold_left (fun (rast:raster columns lines) (p:Z*Z) => setRaster rast true (Z.to_nat (fst p)) (Z.to_nat (snd p))) (let (p) := points in p) (emptyRaster columns lines).
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterQ CoRN.reals.fast.Interval CoRN.logic.Classic CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs Coq.QArith.Qround