proposition: Lemma setRaster_correct2 : forall n m (r:raster n m) x i j i0 j0, raster_well_formed r -> (i <> i0) \/ (j <> j0) -> RasterIndex (setRaster r x i0 j0) i j = RasterIndex r i j.
proof: Proof. intros n m r x i j i0 j0 rWf H. destruct (le_lt_dec (Pos.to_nat m) i0) as [Hm | Hm]. rewrite setRaster_overflow; auto with *. destruct (le_lt_dec (Pos.to_nat n) j0) as [Hn | Hn]. rewrite setRaster_overflow; auto with *. destruct r as [l]. simpl. destruct H. + f_equal. rewrite updateList_correct2. reflexivity. exact H. + destruct rWf. destruct (Nat.eq_dec i i0). subst i0. rewrite updateList_correct1 with (d2:=nil). 2: rewrite H0; exact Hm. rewrite updateList_correct2. reflexivity. exact H. f_equal. rewrite updateList_correct2. reflexivity. exact n0. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos