proposition: Lemma rasterize2_origin : forall n m (t l b r : Q), b < t -> rasterize2 n m t l b r (pair l t) = pair 0%Z 0%Z.
proof: Proof. assert (forall n:positive, 0 <= Zpos n -1)%Z. { intro n. change 0%Z with (1-1)%Z. apply Z.add_le_mono_r. apply Pos.le_1_l. } intros. unfold rasterize2, fst, snd. rewrite rasterize1_origin. replace (rasterize1 b t m t) with (Zpos m)%Z. change (Z.max 0 0) with 0%Z. rewrite Z.max_r. 2: discriminate. rewrite Z.min_l. rewrite Z.min_r. rewrite Z.sub_diag. reflexivity. apply H. rewrite <- (Z.add_0_r (Zpos m)) at 2. apply Z.add_le_mono_l. discriminate. unfold rasterize1. unfold Qdiv. rewrite <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. rewrite Qfloor_Z. reflexivity. intro abs. apply Qlt_minus_iff in H0. unfold Qminus in abs. rewrite abs in H0. exact (Qlt_irrefl 0 H0). 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