[STATEMENT]
lemma col_sylvester_sub: (* TODO: from this directly derive col_sylvester *)
  assumes j: "j < m + n"
  shows "col (sylvester_mat_sub m n p q) j =
    vec_of_poly_rev_shifted p n m j @\<^sub>v vec_of_poly_rev_shifted q m n j" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (sylvester_mat_sub m n p q) j = Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) \<Longrightarrow> col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i
 2. dim_vec (col (sylvester_mat_sub m n p q) j) = dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j)
[PROOF STEP]
show "dim_vec ?l = dim_vec ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (col (sylvester_mat_sub m n p q) j) = dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (col (sylvester_mat_sub m n p q) j) = dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) \<Longrightarrow> col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) \<Longrightarrow> col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i
[PROOF STEP]
assume "i < dim_vec ?r"
[PROOF STATE]
proof (state)
this:
i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) \<Longrightarrow> col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j)
[PROOF STEP]
have i: "i < m+n"
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j)

goal (1 subgoal):
 1. i < m + n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < m + n

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) \<Longrightarrow> col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i
[PROOF STEP]
show "?l $ i = ?r $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i
[PROOF STEP]
unfolding vec_of_poly_rev_shifted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (sylvester_mat_sub m n p q) j $ i = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply (subst index_col)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < dim_row (sylvester_mat_sub m n p q)
 2. j < dim_col (sylvester_mat_sub m n p q)
 3. sylvester_mat_sub m n p q $$ (i, j) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (3 subgoals):
 1. i < dim_row (sylvester_mat_sub m n p q)
 2. j < dim_col (sylvester_mat_sub m n p q)
 3. sylvester_mat_sub m n p q $$ (i, j) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. j < dim_col (sylvester_mat_sub m n p q)
 2. sylvester_mat_sub m n p q $$ (i, j) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j < m + n

goal (2 subgoals):
 1. j < dim_col (sylvester_mat_sub m n p q)
 2. sylvester_mat_sub m n p q $$ (i, j) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sylvester_mat_sub m n p q $$ (i, j) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply (subst sylvester_mat_sub_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < m + n
 2. j < m + n
 3. (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (3 subgoals):
 1. i < m + n
 2. j < m + n
 3. (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. j < m + n
 2. (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j < m + n

goal (2 subgoals):
 1. j < m + n
 2. (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply (cases "i < n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < n \<Longrightarrow> (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
 2. \<not> i < n \<Longrightarrow> (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (2 subgoals):
 1. i < n \<Longrightarrow> (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
 2. \<not> i < n \<Longrightarrow> (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i < n \<Longrightarrow> (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (1 subgoal):
 1. \<not> i < n \<Longrightarrow> (if i < n then if i \<le> j \<and> j - i \<le> m then coeff p (m + i - j) else (0::'a) else if i - n \<le> j \<and> j \<le> i then coeff q (i - j) else (0::'a)) = (vec n (\<lambda>i. if i \<le> j \<and> j \<le> m + i then coeff p (m + i - j) else (0::'a)) @\<^sub>v vec m (\<lambda>i. if i \<le> j \<and> j \<le> n + i then coeff q (n + i - j) else (0::'a))) $ i
[PROOF STEP]
apply (auto simp: not_less not_le intro!: coeff_eq_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
col (sylvester_mat_sub m n p q) j $ i = (Missing_Lemmas.vec_of_poly_rev_shifted p n m j @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n j) $ i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_poly_rev_shifted_scalar_prod:
  fixes p v
  defines "q \<equiv> poly_of_vec v"
  assumes m: "degree p \<le> m" and n: "dim_vec v = n"
  assumes j: "j < m+n"
  shows "vec_of_poly_rev_shifted p n m (n+m-Suc j) \<bullet> v = coeff (p * q) j" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
have id1: "\<And> i. m + i - (n + m - Suc j) = i + Suc j - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. m + i - (n + m - Suc j) = i + Suc j - n
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j < m + n

goal (1 subgoal):
 1. \<And>i. m + i - (n + m - Suc j) = i + Suc j - n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m + ?i - (n + m - Suc j) = ?i + Suc j - n

goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
let ?g = "\<lambda> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) *  v $ i else 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
have "?thesis = ((\<Sum>i = 0..<n. ?g i) =
        (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else 0)))" (is "_ = (?l = ?r)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j) = ((\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))))
[PROOF STEP]
unfolding vec_of_poly_rev_shifted_def coeff_mult m scalar_prod_def n q_def
      coeff_poly_of_vec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Sum>i = 0..<n. vec n (\<lambda>i. if i \<le> n + m - Suc j \<and> n + m - Suc j \<le> m + i then coeff p (m + i - (n + m - Suc j)) else (0::'a)) $ i * v $ i) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))) = ((\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))))
[PROOF STEP]
by (subst sum.cong, insert id1, auto)
[PROOF STATE]
proof (state)
this:
(Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j) = ((\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))))

goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j) = ((\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))))

goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
have "..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "?r = (\<Sum>i\<le>j. (if j - i < n then coeff p i * v $ (n - Suc (j - i)) else 0))" (is "_ = sum ?f _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<le>j. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<le>j. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<le>j. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?f {..j} = sum ?f ({i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n})"
      (is "_ = sum _ (?R1 \<union> ?R2)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>j. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n}. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>j. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n}. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>j. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n}. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "\<dots> = sum ?f ?R1 + sum ?f ?R2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n}. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (\<Sum>i | i \<le> j \<and> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) + (\<Sum>i | i \<le> j \<and> \<not> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))
[PROOF STEP]
by (subst sum.union_disjoint, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n}. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (\<Sum>i | i \<le> j \<and> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) + (\<Sum>i | i \<le> j \<and> \<not> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n}. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (\<Sum>i | i \<le> j \<and> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) + (\<Sum>i | i \<le> j \<and> \<not> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?f ?R2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> j \<and> \<not> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (0::'a)
[PROOF STEP]
by (rule sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> j \<and> \<not> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> j \<and> \<not> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?f ?R1 + 0 = sum (\<lambda> i. coeff p i * v $ (i + n - Suc j)) ?R1"
      (is "_ = sum ?F _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> j \<and> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) + (0::'a) = (\<Sum>i | i \<le> j \<and> j - i < n. coeff p i * v $ (i + n - Suc j))
[PROOF STEP]
by (subst sum.cong, auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> j \<and> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) + (0::'a) = (\<Sum>i | i \<le> j \<and> j - i < n. coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> j \<and> j - i < n. if j - i < n then coeff p i * v $ (n - Suc (j - i)) else (0::'a)) + (0::'a) = (\<Sum>i | i \<le> j \<and> j - i < n. coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "\<dots> = sum ?F ((?R1 \<inter> {..m}) \<union> (?R1 - {..m}))"
      (is "_ = sum _ (?R \<union> ?R')")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<le> j \<and> j - i < n. coeff p i * v $ (i + n - Suc j)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m} \<union> ({i. i \<le> j \<and> j - i < n} - {..m}). coeff p i * v $ (i + n - Suc j))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> j \<and> j - i < n. coeff p i * v $ (i + n - Suc j)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m} \<union> ({i. i \<le> j \<and> j - i < n} - {..m}). coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<le> j \<and> j - i < n. coeff p i * v $ (i + n - Suc j)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m} \<union> ({i. i \<le> j \<and> j - i < n} - {..m}). coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "\<dots> = sum ?F ?R + sum ?F ?R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m} \<union> ({i. i \<le> j \<and> j - i < n} - {..m}). coeff p i * v $ (i + n - Suc j)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j)) + (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j))
[PROOF STEP]
by (subst sum.union_disjoint, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m} \<union> ({i. i \<le> j \<and> j - i < n} - {..m}). coeff p i * v $ (i + n - Suc j)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j)) + (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m} \<union> ({i. i \<le> j \<and> j - i < n} - {..m}). coeff p i * v $ (i + n - Suc j)) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j)) + (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?F ?R' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
assume "x > m"
[PROOF STATE]
proof (state)
this:
m < x

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
degree p \<le> m
m < x
[PROOF STEP]
have "?F x = 0"
[PROOF STATE]
proof (prove)
using this:
degree p \<le> m
m < x

goal (1 subgoal):
 1. coeff p x * v $ (x + n - Suc j) = (0::'a)
[PROOF STEP]
by (subst coeff_eq_0, auto)
[PROOF STATE]
proof (state)
this:
coeff p x * v $ (x + n - Suc j) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
m < ?x2 \<Longrightarrow> coeff p ?x2 * v $ (?x2 + n - Suc j) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m < ?x2 \<Longrightarrow> coeff p ?x2 * v $ (?x2 + n - Suc j) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)
[PROOF STEP]
by (subst sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} - {..m}. coeff p i * v $ (i + n - Suc j)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j)) + (0::'a)
[PROOF STEP]
have r: "?r = sum ?F ?R"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j)) + (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "?l = sum ?g ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i}
      \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)})"
      (is "_ = sum _ (?L1 \<union> ?L2)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)}. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)}. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)}. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "\<dots> = sum ?g ?L1 + sum ?g ?L2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)}. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) + (\<Sum>i | i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i). if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a))
[PROOF STEP]
by (subst sum.union_disjoint, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)}. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) + (\<Sum>i | i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i). if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)}. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) + (\<Sum>i | i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i). if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a))

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?g ?L2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i). if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (0::'a)
[PROOF STEP]
by (rule sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i). if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i). if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?g ?L1 + 0 = sum (\<lambda> i. coeff p (i + Suc j - n) * v $ i) ?L1"
      (is "_ = sum ?G _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) + (0::'a) = (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. coeff p (i + Suc j - n) * v $ i)
[PROOF STEP]
by (subst sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) + (0::'a) = (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) + (0::'a) = (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "\<dots> = sum ?G (?L1 \<inter> {i. i + Suc j - n \<le> m} \<union> (?L1 - {i. i + Suc j - n \<le> m}))"
      (is "_ = sum _ (?L \<union> ?L')")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m} \<union> ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}). coeff p (i + Suc j - n) * v $ i)
[PROOF STEP]
by (subst sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m} \<union> ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}). coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i. coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m} \<union> ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}). coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "\<dots> = sum ?G ?L + sum ?G ?L'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m} \<union> ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}). coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) + (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i)
[PROOF STEP]
by (subst sum.union_disjoint, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m} \<union> ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}). coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) + (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m} \<union> ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}). coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) + (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "sum ?G ?L' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
assume "x + Suc j - n > m"
[PROOF STATE]
proof (state)
this:
m < x + Suc j - n

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
degree p \<le> m
m < x + Suc j - n
[PROOF STEP]
have "?G x = 0"
[PROOF STATE]
proof (prove)
using this:
degree p \<le> m
m < x + Suc j - n

goal (1 subgoal):
 1. coeff p (x + Suc j - n) * v $ x = (0::'a)
[PROOF STEP]
by (subst coeff_eq_0, auto)
[PROOF STATE]
proof (state)
this:
coeff p (x + Suc j - n) * v $ x = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
m < ?x2 + Suc j - n \<Longrightarrow> coeff p (?x2 + Suc j - n) * v $ ?x2 = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m < ?x2 + Suc j - n \<Longrightarrow> coeff p (?x2 + Suc j - n) * v $ ?x2 = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)
[PROOF STEP]
by (subst sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} - {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) + (0::'a)
[PROOF STEP]
have l: "?l = sum ?G ?L"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) + (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i)

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
let ?bij = "\<lambda> i. i + n - Suc j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
assume x: "j < m + n" "Suc (x + j) - n \<le> m" "x < n" "n - Suc j \<le> x"
[PROOF STATE]
proof (state)
this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
define y where "y = x + Suc j - n"
[PROOF STATE]
proof (state)
this:
y = x + Suc j - n

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x
[PROOF STEP]
have "x + Suc j \<ge> n"
[PROOF STATE]
proof (prove)
using this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x

goal (1 subgoal):
 1. n \<le> x + Suc j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<le> x + Suc j

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x
n \<le> x + Suc j
[PROOF STEP]
have xy: "x = ?bij y"
[PROOF STATE]
proof (prove)
using this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x
n \<le> x + Suc j

goal (1 subgoal):
 1. x = y + n - Suc j
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x
n \<le> x + Suc j

goal (1 subgoal):
 1. x = x + Suc j - n + n - Suc j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y + n - Suc j

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x
[PROOF STEP]
have y: "y \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x

goal (1 subgoal):
 1. y \<in> {i. i \<le> j \<and> j - i < n} \<inter> {..m}
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
j < m + n
Suc (x + j) - n \<le> m
x < n
n - Suc j \<le> x

goal (1 subgoal):
 1. x + Suc j - n \<in> {i. i \<le> j \<and> j - i < n} \<inter> {..m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> {i. i \<le> j \<and> j - i < n} \<inter> {..m}

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
have "x \<in> ?bij ` ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>i. i + n - Suc j) ` ({i. i \<le> j \<and> j - i < n} \<inter> {..m})
[PROOF STEP]
unfolding xy
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + n - Suc j \<in> (\<lambda>i. i + n - Suc j) ` ({i. i \<le> j \<and> j - i < n} \<inter> {..m})
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
y \<in> {i. i \<le> j \<and> j - i < n} \<inter> {..m}

goal (1 subgoal):
 1. y + n - Suc j \<in> (\<lambda>i. i + n - Suc j) ` ({i. i \<le> j \<and> j - i < n} \<inter> {..m})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>i. i + n - Suc j) ` ({i. i \<le> j \<and> j - i < n} \<inter> {..m})

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>j < m + n; Suc (?x2 + j) - n \<le> m; ?x2 < n; n - Suc j \<le> ?x2\<rbrakk> \<Longrightarrow> ?x2 \<in> (\<lambda>i. i + n - Suc j) ` ({i. i \<le> j \<and> j - i < n} \<inter> {..m})

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
note tedious = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>j < m + n; Suc (?x2 + j) - n \<le> m; ?x2 < n; n - Suc j \<le> ?x2\<rbrakk> \<Longrightarrow> ?x2 \<in> (\<lambda>i. i + n - Suc j) ` ({i. i \<le> j \<and> j - i < n} \<inter> {..m})

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))
[PROOF STEP]
unfolding l r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} \<inter> {i. i + Suc j - n \<le> m}. coeff p (i + Suc j - n) * v $ i) = (\<Sum>i\<in>{i. i \<le> j \<and> j - i < n} \<inter> {..m}. coeff p i * v $ (i + n - Suc j))
[PROOF STEP]
by (rule sum.reindex_cong[of ?bij], insert j, auto simp: inj_on_def tedious)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) * v $ i else (0::'a)) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a)))

goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j) = ((\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j) = ((\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))) = (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else (0::'a))))

goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc j) \<bullet> v = coeff (p * q) j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sylvester_sub_poly:
  fixes p q :: "'a :: comm_semiring_0 poly"
  assumes m: "degree p \<le> m"
  assumes n: "degree q \<le> n"
  assumes v: "v \<in> carrier_vec (m+n)"
  shows "poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) =
    poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) = poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q
[PROOF STEP]
proof (rule poly_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) na = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) na
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) na = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) na
[PROOF STEP]
let ?Tv = "(sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) na = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) na
[PROOF STEP]
have dim: "dim_vec (vec_first v n) = n" "dim_vec (vec_last v m) = m" "dim_vec ?Tv = n + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_first v n) = n &&& dim_vec (vec_last v m) = m &&& dim_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) = n + m
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (m + n)

goal (1 subgoal):
 1. dim_vec (vec_first v n) = n &&& dim_vec (vec_last v m) = m &&& dim_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) = n + m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (vec_first v n) = n
dim_vec (vec_last v m) = m
dim_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) = n + m

goal (1 subgoal):
 1. \<And>na. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) na = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) na
[PROOF STEP]
have if_distrib: "\<And> x y z. (if x then y else (0 :: 'a)) * z = (if x then y * z else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. (if x then y else (0::'a)) * z = (if x then y * z else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if ?x then ?y else (0::'a)) * ?z = (if ?x then ?y * ?z else (0::'a))

goal (1 subgoal):
 1. \<And>na. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) na = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) na
[PROOF STEP]
show "coeff ?l i = coeff ?r i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
proof (cases "i < m+n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < m + n

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
hence i_mn: "i \<ge> m+n"
        and i_n: "\<And>x. x \<le> i \<and> x < n \<longleftrightarrow> x < n"
        and i_m: "\<And>x. x \<le> i \<and> x < m \<longleftrightarrow> x < m"
[PROOF STATE]
proof (prove)
using this:
\<not> i < m + n

goal (1 subgoal):
 1. m + n \<le> i &&& (\<And>x. (x \<le> i \<and> x < n) = (x < n)) &&& (\<And>x. (x \<le> i \<and> x < m) = (x < m))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m + n \<le> i
(?x \<le> i \<and> ?x < n) = (?x < n)
(?x \<le> i \<and> ?x < m) = (?x < m)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
have "coeff ?r i =
            (\<Sum> x < n. vec_first v n $ (n - Suc x) * coeff p (i - x)) +
            (\<Sum> x < m. vec_last v m $ (m - Suc x) * coeff q (i - x))"
        (is "_ = sum ?f _ + sum ?g _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
unfolding coeff_add coeff_mult Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<le>i. coeff (poly_of_vec (vec_first v n)) ia * coeff p (i - ia)) + (\<Sum>ia\<le>i. coeff (poly_of_vec (vec_last v m)) ia * coeff q (i - ia)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
unfolding coeff_poly_of_vec dim if_distrib
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<le>i. if ia < n then vec_first v n $ (n - Suc ia) * coeff p (i - ia) else (0::'a)) + (\<Sum>ia\<le>i. if ia < m then vec_last v m $ (m - Suc ia) * coeff q (i - ia) else (0::'a)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
unfolding atMost_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{x. x \<le> i}. if ia < n then vec_first v n $ (n - Suc ia) * coeff p (i - ia) else (0::'a)) + (\<Sum>ia\<in>{x. x \<le> i}. if ia < m then vec_last v m $ (m - Suc ia) * coeff q (i - ia) else (0::'a)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
apply(subst sum.inter_filter[symmetric],simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{x \<in> {x. x \<le> i}. x < n}. vec_first v n $ (n - Suc ia) * coeff p (i - ia)) + (\<Sum>ia\<in>{x. x \<le> i}. if ia < m then vec_last v m $ (m - Suc ia) * coeff q (i - ia) else (0::'a)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
apply(subst sum.inter_filter[symmetric],simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{x \<in> {x. x \<le> i}. x < n}. vec_first v n $ (n - Suc ia) * coeff p (i - ia)) + (\<Sum>ia\<in>{x \<in> {x. x \<le> i}. x < m}. vec_last v m $ (m - Suc ia) * coeff q (i - ia)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
unfolding mem_Collect_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{x. x \<le> i \<and> x < n}. vec_first v n $ (n - Suc ia) * coeff p (i - ia)) + (\<Sum>ia\<in>{x. x \<le> i \<and> x < m}. vec_last v m $ (m - Suc ia) * coeff q (i - ia)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
unfolding i_n i_m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{x. x < n}. vec_first v n $ (n - Suc ia) * coeff p (i - ia)) + (\<Sum>ia\<in>{x. x < m}. vec_last v m $ (m - Suc ia) * coeff q (i - ia)) = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
unfolding lessThan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia\<in>{x. x < n}. vec_first v n $ (n - Suc ia) * coeff p (i - ia)) + (\<Sum>ia\<in>{x. x < m}. vec_last v m $ (m - Suc ia) * coeff q (i - ia)) = (\<Sum>x | x < n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x | x < m. vec_last v m $ (m - Suc x) * coeff q (i - x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) + (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x))

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
assume x: "x < n"
[PROOF STATE]
proof (state)
this:
x < n

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
have "coeff p (i-x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p (i - x) = (0::'a)
[PROOF STEP]
apply(rule coeff_eq_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree p < i - x
[PROOF STEP]
using i_mn x m
[PROOF STATE]
proof (prove)
using this:
m + n \<le> i
x < n
degree p \<le> m

goal (1 subgoal):
 1. degree p < i - x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff p (i - x) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
hence "?f x = 0"
[PROOF STATE]
proof (prove)
using this:
coeff p (i - x) = (0::'a)

goal (1 subgoal):
 1. vec_first v n $ (n - Suc x) * coeff p (i - x) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_first v n $ (n - Suc x) * coeff p (i - x) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 < n \<Longrightarrow> vec_first v n $ (n - Suc ?x2) * coeff p (i - ?x2) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
hence "sum ?f {..<n} = 0"
[PROOF STATE]
proof (prove)
using this:
?x2 < n \<Longrightarrow> vec_first v n $ (n - Suc ?x2) * coeff p (i - ?x2) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>x<n. vec_first v n $ (n - Suc x) * coeff p (i - x)) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
assume x: "x < m"
[PROOF STATE]
proof (state)
this:
x < m

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
have "coeff q (i-x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff q (i - x) = (0::'a)
[PROOF STEP]
apply(rule coeff_eq_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q < i - x
[PROOF STEP]
using i_mn x n
[PROOF STATE]
proof (prove)
using this:
m + n \<le> i
x < m
degree q \<le> n

goal (1 subgoal):
 1. degree q < i - x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff q (i - x) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
hence "?g x = 0"
[PROOF STATE]
proof (prove)
using this:
coeff q (i - x) = (0::'a)

goal (1 subgoal):
 1. vec_last v m $ (m - Suc x) * coeff q (i - x) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_last v m $ (m - Suc x) * coeff q (i - x) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 < m \<Longrightarrow> vec_last v m $ (m - Suc ?x2) * coeff q (i - ?x2) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
hence "sum ?g {..<m} = 0"
[PROOF STATE]
proof (prove)
using this:
?x2 < m \<Longrightarrow> vec_last v m $ (m - Suc ?x2) * coeff q (i - ?x2) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x)) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x<m. vec_last v m $ (m - Suc x) * coeff q (i - x)) = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (0::'a) + (0::'a)
[PROOF STEP]
have "coeff ?r i = 0"
[PROOF STATE]
proof (prove)
using this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (0::'a) + (0::'a)

goal (1 subgoal):
 1. coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = (0::'a)

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> i < m + n
[PROOF STEP]
have "0 = coeff ?l i"
[PROOF STATE]
proof (prove)
using this:
\<not> i < m + n

goal (1 subgoal):
 1. (0::'a) = coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i
[PROOF STEP]
unfolding coeff_poly_of_vec dim sum.distrib[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<not> i < m + n

goal (1 subgoal):
 1. (0::'a) = (if i < n + m then ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i) else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) = coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i

goal (2 subgoals):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
 2. \<not> i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i = coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i

goal (1 subgoal):
 1. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < m + n

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
hence "coeff ?l i = ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i)"
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (1 subgoal):
 1. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i)
[PROOF STEP]
unfolding coeff_poly_of_vec dim sum.distrib[symmetric]
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (1 subgoal):
 1. (if i < n + m then ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i) else (0::'a)) = ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i)

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i)

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
have "... = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i) = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply(subst index_mult_mat_vec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n + m - Suc i < dim_row (sylvester_mat_sub m n p q)\<^sup>T
 2. row (sylvester_mat_sub m n p q)\<^sup>T (n + m - Suc i) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (2 subgoals):
 1. n + m - Suc i < dim_row (sylvester_mat_sub m n p q)\<^sup>T
 2. row (sylvester_mat_sub m n p q)\<^sup>T (n + m - Suc i) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (sylvester_mat_sub m n p q)\<^sup>T (n + m - Suc i) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply(subst row_transpose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n + m - Suc i < dim_col (sylvester_mat_sub m n p q)
 2. col (sylvester_mat_sub m n p q) (n + m - Suc i) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (2 subgoals):
 1. n + m - Suc i < dim_col (sylvester_mat_sub m n p q)
 2. col (sylvester_mat_sub m n p q) (n + m - Suc i) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (sylvester_mat_sub m n p q) (n + m - Suc i) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply(subst col_sylvester_sub)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n + m - Suc i < m + n
 2. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i)) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (2 subgoals):
 1. n + m - Suc i < m + n
 2. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i)) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i)) \<bullet> v = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply(subst vec_first_last_append[of v n m,symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. v \<in> carrier_vec (n + m)
 2. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i)) \<bullet> (vec_first v n @\<^sub>v vec_last v m) = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (m + n)

goal (2 subgoals):
 1. v \<in> carrier_vec (n + m)
 2. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i)) \<bullet> (vec_first v n @\<^sub>v vec_last v m) = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply(simp add: add.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) @\<^sub>v Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i)) \<bullet> (vec_first v n @\<^sub>v vec_last v m) = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply(subst scalar_prod_append)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) \<in> carrier_vec ?n1.55
 2. Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i) \<in> carrier_vec ?n2.55
 3. vec_first v n \<in> carrier_vec ?n1.55
 4. vec_last v m \<in> carrier_vec ?n2.55
 5. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) \<bullet> vec_first v n + Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i) \<bullet> vec_last v m = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply (rule carrier_vecI,simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.vec_of_poly_rev_shifted p n m (n + m - Suc i) \<bullet> vec_first v n + Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i) \<bullet> vec_last v m = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply (subst vec_of_poly_rev_shifted_scalar_prod[OF m],simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < m + n
 2. coeff (p * poly_of_vec (vec_first v n)) i + Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i) \<bullet> vec_last v m = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (2 subgoals):
 1. i < m + n
 2. coeff (p * poly_of_vec (vec_first v n)) i + Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i) \<bullet> vec_last v m = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n)) i + Missing_Lemmas.vec_of_poly_rev_shifted q m n (n + m - Suc i) \<bullet> vec_last v m = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply (subst add.commute[of n m])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n)) i + Missing_Lemmas.vec_of_poly_rev_shifted q m n (m + n - Suc i) \<bullet> vec_last v m = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply (subst vec_of_poly_rev_shifted_scalar_prod[OF n])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. dim_vec (vec_last v m) = m
 2. i < n + m
 3. coeff (p * poly_of_vec (vec_first v n)) i + coeff (q * poly_of_vec (vec_last v m)) i = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < n + m
 2. coeff (p * poly_of_vec (vec_first v n)) i + coeff (q * poly_of_vec (vec_last v m)) i = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < m + n

goal (2 subgoals):
 1. i < n + m
 2. coeff (p * poly_of_vec (vec_first v n)) i + coeff (q * poly_of_vec (vec_last v m)) i = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n)) i + coeff (q * poly_of_vec (vec_last v m)) i = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i) = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i) = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
have "... =
        (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else 0) * coeff p (i - x)) +
        (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else 0) * coeff q (i - x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i = (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x))
[PROOF STEP]
unfolding coeff_poly_of_vec[of "vec_first v n",unfolded dim_vec_first,symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i = (\<Sum>x\<le>i. coeff (poly_of_vec (vec_first v n)) x * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x))
[PROOF STEP]
unfolding coeff_poly_of_vec[of "vec_last v m",unfolded dim_vec_last,symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i = (\<Sum>x\<le>i. coeff (poly_of_vec (vec_first v n)) x * coeff p (i - x)) + (\<Sum>x\<le>i. coeff (poly_of_vec (vec_last v m)) x * coeff q (i - x))
[PROOF STEP]
unfolding coeff_mult[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i = coeff (poly_of_vec (vec_first v n) * p) i + coeff (poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i = (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x))

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i = (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x))

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
have "... = coeff ?r i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x)) = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
unfolding coeff_add coeff_mult Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x)) = (\<Sum>ia\<le>i. coeff (poly_of_vec (vec_first v n)) ia * coeff p (i - ia)) + (\<Sum>ia\<le>i. coeff (poly_of_vec (vec_last v m)) ia * coeff q (i - ia))
[PROOF STEP]
unfolding coeff_poly_of_vec dim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x)) = (\<Sum>ia\<le>i. (if ia < n then vec_first v n $ (n - Suc ia) else (0::'a)) * coeff p (i - ia)) + (\<Sum>ia\<le>i. (if ia < m then vec_last v m $ (m - Suc ia) else (0::'a)) * coeff q (i - ia))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else (0::'a)) * coeff p (i - x)) + (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else (0::'a)) * coeff q (i - x)) = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i

goal (1 subgoal):
 1. i < m + n \<Longrightarrow> coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i

goal (1 subgoal):
 1. coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coeff (poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v)) i = coeff (poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q) i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normalize_field [simp]: "normalize (a :: 'a :: {field, semiring_gcd}) = (if a = 0 then 0 else 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize a = (if a = (0::'a) then 0::'a else (1::'a))
[PROOF STEP]
using unit_factor_normalize
[PROOF STATE]
proof (prove)
using this:
?a \<noteq> (0::?'a) \<Longrightarrow> unit_factor (normalize ?a) = (1::?'a)

goal (1 subgoal):
 1. normalize a = (if a = (0::'a) then 0::'a else (1::'a))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma content_field [simp]: "content (p :: 'a :: {field,semiring_gcd} poly) = (if p = 0 then 0 else 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content p = (if p = 0 then 0::'a else (1::'a))
[PROOF STEP]
by (induct p, auto simp: content_def)


[STATEMENT]
lemma primitive_part_field [simp]: "primitive_part (p :: 'a :: {field,semiring_gcd} poly) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primitive_part p = p
[PROOF STEP]
by (cases "p = 0", auto intro!: primitive_part_prim)


[STATEMENT]
lemma primitive_part_dvd: "primitive_part a dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primitive_part a dvd a
[PROOF STEP]
by (metis content_times_primitive_part dvd_def dvd_refl mult_smult_right)


[STATEMENT]
lemma degree_abs [simp]:
  "degree \<bar>p\<bar> = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree \<bar>p\<bar> = degree p
[PROOF STEP]
by (auto simp: abs_poly_def)


[STATEMENT]
lemma degree_gcd1:
  assumes a_not0: "a \<noteq> 0"
  shows "degree (gcd a b) \<le> degree a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
let ?g = "gcd a b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
have gcd_dvd_b: "?g dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd a b dvd a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd a b dvd a

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
gcd a b dvd a
[PROOF STEP]
obtain c where a_gc: "a = ?g * c"
[PROOF STATE]
proof (prove)
using this:
gcd a b dvd a

goal (1 subgoal):
 1. (\<And>c. a = gcd a b * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. a = gcd a b * k

goal (1 subgoal):
 1. (\<And>c. a = gcd a b * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = gcd a b * c

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
have g_not0: "?g \<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd a b \<noteq> 0
[PROOF STEP]
using a_not0 a_gc
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
a = gcd a b * c

goal (1 subgoal):
 1. gcd a b \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gcd a b \<noteq> 0

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
have c0: "c \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0
[PROOF STEP]
using a_not0 a_gc
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
a = gcd a b * c

goal (1 subgoal):
 1. c \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
have "degree ?g \<le> degree (?g * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (gcd a b) \<le> degree (gcd a b * c)
[PROOF STEP]
by (rule degree_mult_right_le[OF c0])
[PROOF STATE]
proof (state)
this:
degree (gcd a b) \<le> degree (gcd a b * c)

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (gcd a b) \<le> degree (gcd a b * c)

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
have "... = degree a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (gcd a b * c) = degree a
[PROOF STEP]
using a_gc
[PROOF STATE]
proof (prove)
using this:
a = gcd a b * c

goal (1 subgoal):
 1. degree (gcd a b * c) = degree a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (gcd a b * c) = degree a

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (gcd a b) \<le> degree a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree (gcd a b) \<le> degree a

goal (1 subgoal):
 1. degree (gcd a b) \<le> degree a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree (gcd a b) \<le> degree a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primitive_part_neg [simp]:
  fixes a::"'a :: {factorial_ring_gcd,factorial_semiring_multiplicative} poly"
  shows "primitive_part (-a) = - primitive_part a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primitive_part (- a) = - primitive_part a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primitive_part (- a) = - primitive_part a
[PROOF STEP]
have "primitive_part (-a) = primitive_part (smult (-1) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primitive_part (- a) = primitive_part (smult (- (1::'a)) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
primitive_part (- a) = primitive_part (smult (- (1::'a)) a)

goal (1 subgoal):
 1. primitive_part (- a) = - primitive_part a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
primitive_part (- a) = primitive_part (smult (- (1::'a)) a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
primitive_part (- a) = primitive_part (smult (- (1::'a)) a)

goal (1 subgoal):
 1. primitive_part (- a) = - primitive_part a
[PROOF STEP]
unfolding primitive_part_smult
[PROOF STATE]
proof (prove)
using this:
primitive_part (- a) = smult (unit_factor (- (1::'a))) (primitive_part a)

goal (1 subgoal):
 1. primitive_part (- a) = - primitive_part a
[PROOF STEP]
by (simp add: is_unit_unit_factor)
[PROOF STATE]
proof (state)
this:
primitive_part (- a) = - primitive_part a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma content_uminus[simp]:
  fixes f::"int poly"
  shows "content (-f) = content f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
have "-f = - (smult 1 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - f = - smult 1 f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- f = - smult 1 f

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- f = - smult 1 f

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
have "... = smult (-1) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - smult 1 f = smult (- 1) f
[PROOF STEP]
using smult_minus_left
[PROOF STATE]
proof (prove)
using this:
smult (- ?a) ?p = - smult ?a ?p

goal (1 subgoal):
 1. - smult 1 f = smult (- 1) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- smult 1 f = smult (- 1) f

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- f = smult (- 1) f
[PROOF STEP]
have "content (-f) = content (smult (-1) f)"
[PROOF STATE]
proof (prove)
using this:
- f = smult (- 1) f

goal (1 subgoal):
 1. content (- f) = content (smult (- 1) f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
content (- f) = content (smult (- 1) f)

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
content (- f) = content (smult (- 1) f)

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
have "... = normalize (- 1) * content f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (smult (- 1) f) = normalize (- 1) * content f
[PROOF STEP]
unfolding content_smult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize (- 1) * content f = normalize (- 1) * content f
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
content (smult (- 1) f) = normalize (- 1) * content f

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
content (- f) = normalize (- 1) * content f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
content (- f) = normalize (- 1) * content f

goal (1 subgoal):
 1. content (- f) = content f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
content (- f) = content f

goal:
No subgoals!
[PROOF STEP]
qed