proposition: Lemma RasterizeQ2_correct : ball (proj1_sig err) (CentersOfPixels (PixelizeQ2 (RasterizeQ2 points n m t l b r)) (l,t) (r,b)) points.
proof: Proof. split. apply Qpos_nonneg. split; intros [x y] Hx. - pose proof (RasterizeQ2_correct2 Hx). intro abs. contradict H; intros [z [Hz0 Hz1]]. specialize (abs z). contradict abs. split. apply InFinEnumC_weaken, Hz0. apply ball_sym, Hz1. - intro abs. pose proof (RasterizeQ2_correct1 Hx). contradict H; intros [z [Hz0 Hz1]]. specialize (abs z). contradict abs. split. apply InFinEnumC_weaken, Hz0. apply ball_sym, Hz1. 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