proposition: Lemma setRaster_wf : forall n m (r:raster n m) x i j, raster_well_formed r -> raster_well_formed (setRaster r x i j).
proof: Proof. intros. destruct r. destruct H. split. - rewrite updateList_length. exact H. - apply Forall_forall. intros. apply In_nth with (d:=nil) in H1. destruct H1 as [k [H1 H2]]. subst x0. rewrite Forall_forall in H0. rewrite updateList_length in H1. destruct (Nat.eq_dec k i). + subst i. rewrite updateList_correct1 with (d2:=nil). rewrite updateList_length. apply H0. apply nth_In, H1. exact H1. + rewrite (updateList_correct2 l). 2: exact n0. apply H0. apply nth_In, H1. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos