proposition: Lemma emptyRasterEmpty : forall n m i j, RasterIndex (emptyRaster n m) i j = false.
proof: Proof. intros n m i j. simpl. rewrite (nth_repeat i (repeat false (Pos.to_nat n)) (Pos.to_nat m) nil). destruct (le_lt_dec (Pos.to_nat m) i). - destruct j; reflexivity. - rewrite (nth_repeat j false (Pos.to_nat n) false). destruct (le_lt_dec (Pos.to_nat n) j); reflexivity. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos