proposition: Lemma setRaster_overflow : forall {n m} (r:raster n m) x i j, raster_well_formed r -> (Pos.to_nat m <= i) \/ (Pos.to_nat n <= j) -> (setRaster r x i j) = r.
proof: Proof. intros. destruct r. unfold setRaster. apply f_equal. destruct H. destruct H0. - apply updateList_overflow. rewrite H. exact H0. - clear H m. rewrite Forall_forall in H1. revert i. induction l. + reflexivity. + intro i. simpl. destruct i. f_equal. apply updateList_overflow. rewrite (H1 a). exact H0. left. reflexivity. f_equal. apply IHl. intros. apply H1. right. exact H. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos