proposition: Lemma RasterizeQ2_wf : forall points n m t l b r, raster_well_formed (PixelizeQ2 (RasterizeQ2 points n m t l b r)).
proof: Proof. intros. unfold PixelizeQ2, RasterizeQ2. pose proof (emptyRaster_wf n m). revert H. generalize (emptyRaster n m). induction points. - intros. exact H. - intros. simpl. apply IHpoints. apply setRaster_wf, H. Qed.
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