[STATEMENT]
lemma vdw_2_right: "vdw k 2 (k+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdw k 2 (k + 1)
[PROOF STEP]
unfolding vdw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b col. a + int (k + 1) \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<k} \<longrightarrow> (\<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b})
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
fix a b :: int and col :: "int \<Rightarrow> nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
assume *: "a + int (k + 1) \<le> b + 1" "col \<in> {a..b} \<rightarrow> {..<k}"
[PROOF STATE]
proof (state)
this:
a + int (k + 1) \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "col ` {a..b} \<subseteq> {..<k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col ` {a..b} \<subseteq> {..<k}
[PROOF STEP]
using *(2)
[PROOF STATE]
proof (prove)
using this:
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. col ` {a..b} \<subseteq> {..<k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col ` {a..b} \<subseteq> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
col ` {a..b} \<subseteq> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "k+1 \<le> card {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + 1 \<le> card {a..b}
[PROOF STEP]
using *(1)
[PROOF STATE]
proof (prove)
using this:
a + int (k + 1) \<le> b + 1

goal (1 subgoal):
 1. k + 1 \<le> card {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k + 1 \<le> card {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
col ` {a..b} \<subseteq> {..<k}
k + 1 \<le> card {a..b}
[PROOF STEP]
have "card (col ` {a..b}) < card {a..b}"
[PROOF STATE]
proof (prove)
using this:
col ` {a..b} \<subseteq> {..<k}
k + 1 \<le> card {a..b}

goal (1 subgoal):
 1. card (col ` {a..b}) < card {a..b}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
col ` {a..b} \<subseteq> {..<k}
k + 1 \<le> card {a..b}
a + int (k + 1) \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. card (col ` {a..b}) < card {a..b}
[PROOF STEP]
by (metis card_lessThan card_mono finite_lessThan le_less_trans
        less_add_one not_le)
[PROOF STATE]
proof (state)
this:
card (col ` {a..b}) < card {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (col ` {a..b}) < card {a..b}
[PROOF STEP]
have "\<not> inj_on col {a..b}"
[PROOF STATE]
proof (prove)
using this:
card (col ` {a..b}) < card {a..b}

goal (1 subgoal):
 1. \<not> inj_on col {a..b}
[PROOF STEP]
using pigeonhole[of col "{a..b}"]
[PROOF STATE]
proof (prove)
using this:
card (col ` {a..b}) < card {a..b}
card (col ` {a..b}) < card {a..b} \<Longrightarrow> \<not> inj_on col {a..b}

goal (1 subgoal):
 1. \<not> inj_on col {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> inj_on col {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on col {a..b}
[PROOF STEP]
obtain start start_step
    where pigeon: "col start = col start_step"
      "start < start_step"
      "start \<in> {a..b}"
      "start_step \<in> {a..b}"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on col {a..b}

goal (1 subgoal):
 1. (\<And>start start_step. \<lbrakk>col start = col start_step; start < start_step; start \<in> {a..b}; start_step \<in> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inj_onI[of "{a..b}" col]
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on col {a..b}
(\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; col x = col y\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> inj_on col {a..b}

goal (1 subgoal):
 1. (\<And>start start_step. \<lbrakk>col start = col start_step; start < start_step; start \<in> {a..b}; start_step \<in> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
col start = col start_step
start < start_step
start \<in> {a..b}
start_step \<in> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define step where "step = nat (start_step - start)"
[PROOF STATE]
proof (state)
this:
step = nat (start_step - start)

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
define j where "j = col start"
[PROOF STATE]
proof (state)
this:
j = col start

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "j < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < k
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col start < k
[PROOF STEP]
using *(2) pigeon(3)
[PROOF STATE]
proof (prove)
using this:
col \<in> {a..b} \<rightarrow> {..<k}
start \<in> {a..b}

goal (1 subgoal):
 1. col start < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < k

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < k

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "0 < step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < step
[PROOF STEP]
unfolding step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < nat (start_step - start)
[PROOF STEP]
using pigeon(2)
[PROOF STATE]
proof (prove)
using this:
start < start_step

goal (1 subgoal):
 1. 0 < nat (start_step - start)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < step

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < step

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "is_arith_prog_on 2 start step a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arith_prog_on 2 start step a b
[PROOF STEP]
unfolding is_arith_prog_on_def arith_prog_def step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> start \<and> start + int ((2 - 1) * nat (start_step - start)) \<le> b
[PROOF STEP]
using pigeon
[PROOF STATE]
proof (prove)
using this:
col start = col start_step
start < start_step
start \<in> {a..b}
start_step \<in> {a..b}

goal (1 subgoal):
 1. a \<le> start \<and> start + int ((2 - 1) * nat (start_step - start)) \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_arith_prog_on 2 start step a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_arith_prog_on 2 start step a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
is_arith_prog_on 2 start step a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "arith_prog start step i \<in> {start, start_step}" if "i<2" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step i \<in> {start, start_step}
[PROOF STEP]
using that arith_prog_def step_def
[PROOF STATE]
proof (prove)
using this:
i < 2
arith_prog ?start ?step ?i = ?start + int (?i * ?step)
step = nat (start_step - start)

goal (1 subgoal):
 1. arith_prog start step i \<in> {start, start_step}
[PROOF STEP]
by (auto simp: less_2_cases_iff)
[PROOF STATE]
proof (state)
this:
?i < 2 \<Longrightarrow> arith_prog start step ?i \<in> {start, start_step}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
?i < 2 \<Longrightarrow> arith_prog start step ?i \<in> {start, start_step}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "\<dots> \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {start, start_step} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
using pigeon
[PROOF STATE]
proof (prove)
using this:
col start = col start_step
start < start_step
start \<in> {a..b}
start_step \<in> {a..b}

goal (1 subgoal):
 1. {start, start_step} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
using this:
col start = col start_step
start < start_step
start \<in> {a..b}
start_step \<in> {a..b}

goal (1 subgoal):
 1. {start, start_step} \<subseteq> col -` {col start} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{start, start_step} \<subseteq> col -` {j} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
?i1 < 2 \<Longrightarrow> arith_prog start step ?i1 \<in> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
using this:
?i1 < 2 \<Longrightarrow> arith_prog start step ?i1 \<in> col -` {j} \<inter> {a..b}

goal (1 subgoal):
 1. arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int (k + 1) \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < k
0 < step
is_arith_prog_on 2 start step a b
arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
show "\<exists>j start step.
          j < k \<and>
          0 < step \<and>
          is_arith_prog_on 2 start step a b \<and>
          arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
using this:
j < k
0 < step
is_arith_prog_on 2 start step a b
arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}

goal (1 subgoal):
 1. \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 2 start step a b \<and> arith_prog start step ` {..<2} \<subseteq> col -` {j} \<inter> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vdw_lemmaE:
  fixes a b :: int
  assumes "vdw_lemma k m l n"
    "b + 1 \<ge> a + int n" "col \<in> {a..b} \<rightarrow> {..<k}"
  obtains start steps where
    "\<And>i. i < m \<Longrightarrow> steps i > 0"
    "is_multi_arith_prog_on (l+1) m start steps a b"
    "let f = multi_arith_prog m start steps
     in  \<forall>c \<in> {0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall> j \<le> s. c j < l) \<longrightarrow>
            col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>steps start. \<lbrakk>\<And>i. i < m \<Longrightarrow> 0 < steps i; is_multi_arith_prog_on (l + 1) m start steps a b; let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
vdw_lemma k m l n
a + int n \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
\<lbrakk>\<And>i. i < m \<Longrightarrow> 0 < ?steps i; is_multi_arith_prog_on (l + 1) m ?start ?steps a b; let f = multi_arith_prog m ?start ?steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>steps start. \<lbrakk>\<And>i. i < m \<Longrightarrow> 0 < steps i; is_multi_arith_prog_on (l + 1) m start steps a b; let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vdw_lemma_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a b col. a + int n \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<k} \<longrightarrow> (\<exists>start steps. (\<forall>i<m. 0 < steps i) \<and> is_multi_arith_prog_on (l + 1) m start steps a b \<and> (let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))))
a + int n \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
\<lbrakk>\<And>i. i < m \<Longrightarrow> 0 < ?steps i; is_multi_arith_prog_on (l + 1) m ?start ?steps a b; let f = multi_arith_prog m ?start ?steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>steps start. \<lbrakk>\<And>i. i < m \<Longrightarrow> 0 < steps i; is_multi_arith_prog_on (l + 1) m start steps a b; let f = multi_arith_prog m start steps in \<forall>c\<in>{0..<m} \<rightarrow> {0..l}. \<forall>s<m. (\<forall>j\<le>s. c j < l) \<longrightarrow> col (f c) = col (f (\<lambda>i. if i \<le> s then 0 else c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma sum_mod_poly:
  assumes "(k::nat)>0"
  shows "(k - 1) * (\<Sum> n\<in>{..<q}. k^n) < k^q "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
have "int ((k - 1) * (\<Sum>n<q. k ^ n)) =
        (int k - 1) * (\<Sum>n<q. int k ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int ((k - 1) * sum ((^) k) {..<q}) = (int k - 1) * sum ((^) (int k)) {..<q}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. int ((k - 1) * sum ((^) k) {..<q}) = (int k - 1) * sum ((^) (int k)) {..<q}
[PROOF STEP]
by (simp add: of_nat_diff)
[PROOF STATE]
proof (state)
this:
int ((k - 1) * sum ((^) k) {..<q}) = (int k - 1) * sum ((^) (int k)) {..<q}

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int ((k - 1) * sum ((^) k) {..<q}) = (int k - 1) * sum ((^) (int k)) {..<q}

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
have "\<dots> = int k ^ q - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int k - 1) * sum ((^) (int k)) {..<q} = int k ^ q - 1
[PROOF STEP]
by (induction q) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
(int k - 1) * sum ((^) (int k)) {..<q} = int k ^ q - 1

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(int k - 1) * sum ((^) (int k)) {..<q} = int k ^ q - 1

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
have "\<dots> < int (k ^ q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int k ^ q - 1 < int (k ^ q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int k ^ q - 1 < int (k ^ q)

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int ((k - 1) * sum ((^) k) {..<q}) < int (k ^ q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
int ((k - 1) * sum ((^) k) {..<q}) < int (k ^ q)

goal (1 subgoal):
 1. (k - 1) * sum ((^) k) {..<q} < k ^ q
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(k - 1) * sum ((^) k) {..<q} < k ^ q

goal:
No subgoals!
[PROOF STEP]
qed