proposition: Lemma rasterize2_bound : forall n z, (0 <= Z.min (Zpos n -1) (Z.max 0 z) < Zpos n)%Z.
proof: Proof. split. - apply Z.min_case. apply Z.le_0_sub, Pos.le_1_l. apply Z.le_max_l. - apply (Z.le_lt_trans _ _ _ (Z.le_min_l _ _)). rewrite <- (Z.add_0_r (Z.pos n)) at 2. apply Z.add_lt_mono_l. reflexivity. 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