proposition: Lemma setRaster_carry : forall l r n m (bm:raster n m) i j, raster_well_formed bm -> Is_true (RasterIndex bm i j) -> Is_true (RasterIndex (setRaster bm true l r) i j).
proof: Proof. intros l r m n bm i j rWf H. destruct (le_lt_dec (Pos.to_nat n) l). rewrite setRaster_overflow; auto. destruct (le_lt_dec (Pos.to_nat m) r). rewrite setRaster_overflow; auto. destruct (eq_nat_dec i l). destruct (eq_nat_dec j r). rewrite e, e0. rewrite setRaster_correct1; try constructor; congruence. rewrite setRaster_correct2; auto. rewrite setRaster_correct2; auto. 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