[STATEMENT]
lemma independent_not_zero_rows_rref:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  shows "vec.independent {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.independent {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
define R where "R = {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
R = {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
assume dep: "vec.dependent R"
[PROOF STATE]
proof (state)
this:
vec.dependent R

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vec.dependent R
[PROOF STEP]
obtain a where a_in_R: "a\<in>R" and a_in_span: "a \<in> vec.span (R - {a})"
[PROOF STATE]
proof (prove)
using this:
vec.dependent R

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> R; a \<in> vec.span (R - {a})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vec.dependent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>R. a \<in> vec.span (R - {a})

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> R; a \<in> vec.span (R - {a})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
a \<in> R
a \<in> vec.span (R - {a})

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
from a_in_R
[PROOF STATE]
proof (chain)
picking this:
a \<in> R
[PROOF STEP]
obtain i where a_eq_row_i_A: "a=row i A"
[PROOF STATE]
proof (prove)
using this:
a \<in> R

goal (1 subgoal):
 1. (\<And>i. a = row i A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
a \<in> {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. (\<And>i. a = row i A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = row i A

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
hence a_eq_Ai: "a = A $ i"
[PROOF STATE]
proof (prove)
using this:
a = row i A

goal (1 subgoal):
 1. a = A $ i
[PROOF STEP]
unfolding row_def
[PROOF STATE]
proof (prove)
using this:
a = vec_lambda (($) (A $ i))

goal (1 subgoal):
 1. a = A $ i
[PROOF STEP]
unfolding vec_nth_inverse
[PROOF STATE]
proof (prove)
using this:
a = A $ i

goal (1 subgoal):
 1. a = A $ i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = A $ i

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have row_i_A_not_zero: "\<not> is_zero_row i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row i A
[PROOF STEP]
using a_in_R
[PROOF STATE]
proof (prove)
using this:
a \<in> R

goal (1 subgoal):
 1. \<not> is_zero_row i A
[PROOF STEP]
unfolding R_def is_zero_row_def is_zero_row_upt_ncols row_def vec_nth_inverse
[PROOF STATE]
proof (prove)
using this:
a \<in> {A $ i |i. A $ i \<noteq> 0}

goal (1 subgoal):
 1. \<not> (\<forall>j. A $ i $ j = (0::'a))
[PROOF STEP]
unfolding vec_lambda_unique zero_vec_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
\<exists>i. a = A $ i \<and> A $ i \<noteq> (\<chi>i. (0::'a))

goal (1 subgoal):
 1. (\<chi>j. (0::'a)) \<noteq> A $ i
[PROOF STEP]
using a_eq_Ai
[PROOF STATE]
proof (prove)
using this:
\<exists>i. a = A $ i \<and> A $ i \<noteq> (\<chi>i. (0::'a))
a = A $ i

goal (1 subgoal):
 1. (\<chi>j. (0::'a)) \<noteq> A $ i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i A

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
define least_n where "least_n = (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (state)
this:
least_n = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have span_rw: "vec.span (R - {a}) = range (\<lambda>u. \<Sum>v\<in>R - {a}. u v *s v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.span (R - {a}) = range (\<lambda>u. \<Sum>v\<in>R - {a}. u v *s v)
[PROOF STEP]
proof (rule vec.span_finite)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (R - {a})
[PROOF STEP]
show "finite (R - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (R - {a})
[PROOF STEP]
using finite_rows[of A]
[PROOF STATE]
proof (prove)
using this:
finite (rows A)

goal (1 subgoal):
 1. finite (R - {a})
[PROOF STEP]
unfolding rows_def R_def
[PROOF STATE]
proof (prove)
using this:
finite {row i A |i. i \<in> UNIV}

goal (1 subgoal):
 1. finite ({row i A |i. row i A \<noteq> 0} - {a})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (R - {a})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vec.span (R - {a}) = range (\<lambda>u. \<Sum>v\<in>R - {a}. u v *s v)

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vec.span (R - {a}) = range (\<lambda>u. \<Sum>v\<in>R - {a}. u v *s v)
[PROOF STEP]
obtain f where f: "(\<Sum>v\<in>(R - {a}). f v *s v) = a"
[PROOF STATE]
proof (prove)
using this:
vec.span (R - {a}) = range (\<lambda>u. \<Sum>v\<in>R - {a}. u v *s v)

goal (1 subgoal):
 1. (\<And>f. (\<Sum>v\<in>R - {a}. f v *s v) = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a_in_span
[PROOF STATE]
proof (prove)
using this:
vec.span (R - {a}) = range (\<lambda>u. \<Sum>v\<in>R - {a}. u v *s v)
a \<in> vec.span (R - {a})

goal (1 subgoal):
 1. (\<And>f. (\<Sum>v\<in>R - {a}. f v *s v) = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) imageE)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. f v *s v) = a

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have "1 = a $ least_n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) = a $ least_n
[PROOF STEP]
using rref_condition2[OF rref_A] row_i_A_not_zero
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row i A

goal (1 subgoal):
 1. (1::'a) = a $ least_n
[PROOF STEP]
unfolding least_n_def a_eq_Ai
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row i A

goal (1 subgoal):
 1. (1::'a) = A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(1::'a) = a $ least_n

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) = a $ least_n

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have"... = (\<Sum>v\<in>(R - {a}). f v *s v) $ least_n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a $ least_n = (\<Sum>v\<in>R - {a}. f v *s v) $ least_n
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
(\<Sum>v\<in>R - {a}. f v *s v) = a

goal (1 subgoal):
 1. a $ least_n = (\<Sum>v\<in>R - {a}. f v *s v) $ least_n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a $ least_n = (\<Sum>v\<in>R - {a}. f v *s v) $ least_n

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a $ least_n = (\<Sum>v\<in>R - {a}. f v *s v) $ least_n

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have "... = (\<Sum>v\<in>(R - {a}). (f v *s v) $ least_n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>R - {a}. f v *s v) $ least_n = (\<Sum>v\<in>R - {a}. (f v *s v) $ least_n)
[PROOF STEP]
unfolding sum_component
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>R - {a}. (f x *s x) $ least_n) = (\<Sum>v\<in>R - {a}. (f v *s v) $ least_n)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. f v *s v) $ least_n = (\<Sum>v\<in>R - {a}. (f v *s v) $ least_n)

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. f v *s v) $ least_n = (\<Sum>v\<in>R - {a}. (f v *s v) $ least_n)

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have "... = (\<Sum>v\<in>(R - {a}). (f v) * (v $ least_n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>R - {a}. (f v *s v) $ least_n) = (\<Sum>v\<in>R - {a}. f v * v $ least_n)
[PROOF STEP]
unfolding vector_smult_component
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>R - {a}. f v * v $ least_n) = (\<Sum>v\<in>R - {a}. f v * v $ least_n)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. (f v *s v) $ least_n) = (\<Sum>v\<in>R - {a}. f v * v $ least_n)

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. (f v *s v) $ least_n) = (\<Sum>v\<in>R - {a}. f v * v $ least_n)

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have "... = (\<Sum>v\<in>(R - {a}). 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>R - {a}. f v * v $ least_n) = (\<Sum>v\<in>R - {a}. (0::'a))
[PROOF STEP]
proof (rule sum.cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. R - {a} = R - {a}
 2. \<And>x. x \<in> R - {a} \<Longrightarrow> f x * x $ least_n = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. R - {a} = R - {a}
 2. \<And>x. x \<in> R - {a} \<Longrightarrow> f x * x $ least_n = (0::'a)
[PROOF STEP]
assume x: "x \<in> R - {a}"
[PROOF STATE]
proof (state)
this:
x \<in> R - {a}

goal (2 subgoals):
 1. R - {a} = R - {a}
 2. \<And>x. x \<in> R - {a} \<Longrightarrow> f x * x $ least_n = (0::'a)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> R - {a}
[PROOF STEP]
obtain j where x_eq_row_j_A: "x=row j A"
[PROOF STATE]
proof (prove)
using this:
x \<in> R - {a}

goal (1 subgoal):
 1. (\<And>j. x = row j A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {row i A |i. row i A \<noteq> 0} - {a}

goal (1 subgoal):
 1. (\<And>j. x = row j A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = row j A

goal (2 subgoals):
 1. R - {a} = R - {a}
 2. \<And>x. x \<in> R - {a} \<Longrightarrow> f x * x $ least_n = (0::'a)
[PROOF STEP]
hence i_not_j: "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
x = row j A

goal (1 subgoal):
 1. i \<noteq> j
[PROOF STEP]
using a_eq_row_i_A x
[PROOF STATE]
proof (prove)
using this:
x = row j A
a = row i A
x \<in> R - {a}

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

goal (2 subgoals):
 1. R - {a} = R - {a}
 2. \<And>x. x \<in> R - {a} \<Longrightarrow> f x * x $ least_n = (0::'a)
[PROOF STEP]
have x_least_is_zero: "x $ least_n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ least_n = (0::'a)
[PROOF STEP]
using rref_condition4[OF rref_A] i_not_j row_i_A_not_zero
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
i \<noteq> j
\<not> is_zero_row i A

goal (1 subgoal):
 1. x $ least_n = (0::'a)
[PROOF STEP]
unfolding x_eq_row_j_A least_n_def row_def vec_nth_inverse
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
i \<noteq> j
\<not> is_zero_row i A

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x $ least_n = (0::'a)

goal (2 subgoals):
 1. R - {a} = R - {a}
 2. \<And>x. x \<in> R - {a} \<Longrightarrow> f x * x $ least_n = (0::'a)
[PROOF STEP]
show "f x * x $ least_n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x * x $ least_n = (0::'a)
[PROOF STEP]
unfolding x_least_is_zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x * (0::'a) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x * x $ least_n = (0::'a)

goal (1 subgoal):
 1. R - {a} = R - {a}
[PROOF STEP]
qed rule
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. f v * v $ least_n) = (\<Sum>v\<in>R - {a}. (0::'a))

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. f v * v $ least_n) = (\<Sum>v\<in>R - {a}. (0::'a))

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>R - {a}. (0::'a)) = (0::'a)
[PROOF STEP]
unfolding sum.neutral_const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) = (0::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>R - {a}. (0::'a)) = (0::'a)

goal (1 subgoal):
 1. vec.dependent {row i A |i. row i A \<noteq> 0} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1::'a) = (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invertible_row_add_iterate:
  fixes A::"'a::{ring_1}^'n^'m::{mod_type}"
  assumes n: "n<nrows A"
  shows "\<exists>P. invertible P \<and> row_add_iterate A n i j = P**A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n < nrows A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
fix A::"'a::{ring_1}^'n^'m::{mod_type}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
show "\<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
proof (cases "i=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
 2. i \<noteq> (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = (0::'m)

goal (2 subgoals):
 1. i = (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
 2. i \<noteq> (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
unfolding row_add_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> (if i = (0::'m) then A else row_add A (0::'m) i (- A $ (0::'m) $ j)) = P ** A
[PROOF STEP]
by (metis True invertible_def matrix_mul_lid)
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A

goal (1 subgoal):
 1. i \<noteq> (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> (0::'m)

goal (1 subgoal):
 1. i \<noteq> (0::'m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A
[PROOF STEP]
by (metis False invertible_row_add row_add_iterate.simps(1) row_add_mat_1)
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> row_add_iterate A 0 i j = P ** A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
fix n and A::"'a::{ring_1}^'n^'m::{mod_type}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
define A' where "A' = row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)"
[PROOF STATE]
proof (state)
this:
A' = row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
assume  hyp: "\<And>A::'a::{ring_1}^'n^'m::{mod_type}. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A" and Suc_n: "Suc n < nrows A"
[PROOF STATE]
proof (state)
this:
n < nrows ?A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate ?A n i j = P ** ?A
Suc n < nrows A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
hence "\<exists>P. invertible P \<and> row_add_iterate A' n i j = P ** A'"
[PROOF STATE]
proof (prove)
using this:
n < nrows ?A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate ?A n i j = P ** ?A
Suc n < nrows A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A' n i j = P ** A'
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
n < CARD('m) \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate ?A n i j = P ** ?A
Suc n < CARD('m)

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A' n i j = P ** A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> row_add_iterate A' n i j = P ** A'

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>P. invertible P \<and> row_add_iterate A' n i j = P ** A'
[PROOF STEP]
obtain P where inv_P: "invertible P"  and P: "row_add_iterate A' n i j = P ** A'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> row_add_iterate A' n i j = P ** A'

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; row_add_iterate A' n i j = P ** A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible P
row_add_iterate A' n i j = P ** A'

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A; Suc n < nrows A\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
show "\<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A
[PROOF STEP]
unfolding row_add_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
proof (cases "Suc n = to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
show "\<exists>P. invertible P \<and>
      (if Suc n = to_nat i then row_add_iterate A n i j
      else row_add_iterate (row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)) n i j) =
      P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
unfolding if_P[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A
[PROOF STEP]
using hyp Suc_n
[PROOF STATE]
proof (prove)
using this:
n < nrows ?A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate ?A n i j = P ** ?A
Suc n < nrows A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate A n i j = P ** A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
show "\<exists>P. invertible P \<and>
      (if Suc n = to_nat i then row_add_iterate A n i j
      else row_add_iterate (row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)) n i j) =
      P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A
[PROOF STEP]
unfolding if_not_P[OF False]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j = P ** A
[PROOF STEP]
unfolding P[unfolded A'_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Pa. invertible Pa \<and> P ** row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) = Pa ** A
[PROOF STEP]
proof (rule exI[of _ "P ** (row_add (mat 1) (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j))"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invertible (P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j))
 2. P ** row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) = P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) ** A
[PROOF STEP]
show "invertible (P ** row_add (mat 1) (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j))
[PROOF STEP]
by (metis False Suc_n inv_P invertible_mult invertible_row_add to_nat_from_nat_id nrows_def)
[PROOF STATE]
proof (state)
this:
invertible (P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j))

goal (1 subgoal):
 1. P ** row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) = P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) ** A
[PROOF STEP]
show "P ** row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j) =
        P ** row_add (mat 1) (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j) ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ** row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) = P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) ** A
[PROOF STEP]
using matrix_mul_assoc row_add_mat_1[of "from_nat (Suc n)" i " (- A $ from_nat (Suc n) $ j)"]
[PROOF STATE]
proof (prove)
using this:
?A ** (?B ** ?C) = ?A ** ?B ** ?C
row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) ** ?A = row_add ?A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. P ** row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) = P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) ** A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P ** row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) = P ** row_add (mat (1::'a)) (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) ** A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = P ** A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> row_add_iterate A (Suc n) i j = P ** A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_add_iterate_preserves_greater_than_n:
  fixes A::"'a::{ring_1}^'n^'m::{mod_type}"
  assumes n: "n<nrows A"
  and a: "to_nat a > n"
  shows "(row_add_iterate A n i j) $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = A $ a $ b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n < nrows A
n < mod_type_class.to_nat a

goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = A $ a $ b
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 < nrows A; 0 < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A 0 i j $ a $ b = A $ a $ b
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < nrows A
0 < mod_type_class.to_nat a

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 < nrows A; 0 < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A 0 i j $ a $ b = A $ a $ b
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A 0 i j $ a $ b = A $ a $ b
[PROOF STEP]
unfolding row_add_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = (0::'m) then A else row_add A (0::'m) i (- A $ (0::'m) $ j)) $ a $ b = A $ a $ b
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> (0::'m) \<Longrightarrow> row_add A (0::'m) i (- A $ (0::'m) $ j) $ a $ b = A $ a $ b
[PROOF STEP]
assume "i \<noteq> 0"
[PROOF STATE]
proof (state)
this:
i \<noteq> (0::'m)

goal (1 subgoal):
 1. i \<noteq> (0::'m) \<Longrightarrow> row_add A (0::'m) i (- A $ (0::'m) $ j) $ a $ b = A $ a $ b
[PROOF STEP]
hence "a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> (0::'m)

goal (1 subgoal):
 1. a \<noteq> (0::'m)
[PROOF STEP]
by (metis "0.prems"(2) less_numeral_extra(3) to_nat_0)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'m)

goal (1 subgoal):
 1. i \<noteq> (0::'m) \<Longrightarrow> row_add A (0::'m) i (- A $ (0::'m) $ j) $ a $ b = A $ a $ b
[PROOF STEP]
thus "row_add A 0 i (- A $ 0 $ j) $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'m)

goal (1 subgoal):
 1. row_add A (0::'m) i (- A $ (0::'m) $ j) $ a $ b = A $ a $ b
[PROOF STEP]
unfolding row_add_def
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'m)

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = (0::'m) then A $ (0::'m) $ ja + - A $ (0::'m) $ j * A $ i $ ja else A $ ia $ ja) $ a $ b = A $ a $ b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_add A (0::'m) i (- A $ (0::'m) $ j) $ a $ b = A $ a $ b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A 0 i j $ a $ b = A $ a $ b

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
fix n and A::"'a::{ring_1}^'n^'m::{mod_type}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
assume hyp: "(\<And>A::'a::{ring_1}^'n^'m::{mod_type}. n < nrows A \<Longrightarrow> n < to_nat a \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b)"
    and suc_n_less_card: "Suc n < nrows A" and suc_n_kess_a: "Suc n < to_nat a"
[PROOF STATE]
proof (state)
this:
\<lbrakk>n < nrows ?A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ a $ b = ?A $ a $ b
Suc n < nrows A
Suc n < mod_type_class.to_nat a

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
hence row_add_iterate_A: "row_add_iterate A n i j $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n < nrows ?A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ a $ b = ?A $ a $ b
Suc n < nrows A
Suc n < mod_type_class.to_nat a

goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = A $ a $ b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_add_iterate A n i j $ a $ b = A $ a $ b

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = A $ a $ b; Suc n < nrows A; Suc n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
show "row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
proof (cases "Suc n = to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
show "row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
unfolding row_add_iterate.simps if_P[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = A $ a $ b
[PROOF STEP]
using row_add_iterate_A
[PROOF STATE]
proof (prove)
using this:
row_add_iterate A n i j $ a $ b = A $ a $ b

goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = A $ a $ b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
define A' where "A' = row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)"
[PROOF STATE]
proof (state)
this:
A' = row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
have row_add_iterate_A': "row_add_iterate A' n i j $ a $ b = A' $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' n i j $ a $ b = A' $ a $ b
[PROOF STEP]
using hyp suc_n_less_card suc_n_kess_a
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n < nrows ?A; n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ a $ b = ?A $ a $ b
Suc n < nrows A
Suc n < mod_type_class.to_nat a

goal (1 subgoal):
 1. row_add_iterate A' n i j $ a $ b = A' $ a $ b
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n < CARD('m); n < mod_type_class.to_nat a\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ a $ b = ?A $ a $ b
Suc n < CARD('m)
Suc n < mod_type_class.to_nat a

goal (1 subgoal):
 1. row_add_iterate A' n i j $ a $ b = A' $ a $ b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_add_iterate A' n i j $ a $ b = A' $ a $ b

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
have from_nat_not_a: "from_nat (Suc n) \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) \<noteq> a
[PROOF STEP]
by (metis less_not_refl suc_n_kess_a suc_n_less_card to_nat_from_nat_id nrows_def)
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (Suc n) \<noteq> a

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
show "row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b
[PROOF STEP]
unfolding row_add_iterate.simps if_not_P[OF False] row_add_iterate_A'[unfolded A'_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ a $ b = A $ a $ b
[PROOF STEP]
unfolding row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ b = A $ a $ b
[PROOF STEP]
using from_nat_not_a
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat (Suc n) \<noteq> a

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ b = A $ a $ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ a $ b = A $ a $ b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_add_iterate_preserves_pivot_row:
  fixes A::"'a::{ring_1}^'n^'m::{mod_type}"
  assumes n: "n<nrows A"
  and a: "to_nat i \<le> n"
  shows "(row_add_iterate A n i j) $ i $ b = A $ i $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A n i j $ i $ b = A $ i $ b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n < nrows A
mod_type_class.to_nat i \<le> n

goal (1 subgoal):
 1. row_add_iterate A n i j $ i $ b = A $ i $ b
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 < nrows A; mod_type_class.to_nat i \<le> 0\<rbrakk> \<Longrightarrow> row_add_iterate A 0 i j $ i $ b = A $ i $ b
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b; Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < nrows A
mod_type_class.to_nat i \<le> 0

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 < nrows A; mod_type_class.to_nat i \<le> 0\<rbrakk> \<Longrightarrow> row_add_iterate A 0 i j $ i $ b = A $ i $ b
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b; Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A 0 i j $ i $ b = A $ i $ b
[PROOF STEP]
by (metis "0.prems"(2) le_0_eq least_mod_type row_add_iterate.simps(1) to_nat_eq to_nat_mono')
[PROOF STATE]
proof (state)
this:
row_add_iterate A 0 i j $ i $ b = A $ i $ b

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b; Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b; Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
fix n and A::"'a::{ring_1}^'n^'m::{mod_type}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b; Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
assume hyp: "\<And>A::'a::{ring_1}^'n^'m::{mod_type}. n < nrows A \<Longrightarrow> to_nat i \<le> n \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b"
    and Suc_n_less_card: "Suc n < nrows A" and i_less_suc: "to_nat i \<le> Suc n"
[PROOF STATE]
proof (state)
this:
\<lbrakk>n < nrows ?A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ i $ b = ?A $ i $ b
Suc n < nrows A
mod_type_class.to_nat i \<le> Suc n

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ i $ b = A $ i $ b; Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
show "row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
proof (cases "Suc n = to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
unfolding row_add_iterate.simps if_P[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A n i j $ i $ b = A $ i $ b
[PROOF STEP]
apply (rule row_add_iterate_preserves_greater_than_n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < nrows A
 2. n < mod_type_class.to_nat i
[PROOF STEP]
using Suc_n_less_card True lessI
[PROOF STATE]
proof (prove)
using this:
Suc n < nrows A
Suc n = mod_type_class.to_nat i
?n < Suc ?n

goal (2 subgoals):
 1. n < nrows A
 2. n < mod_type_class.to_nat i
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
define A' where "A' = row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)"
[PROOF STATE]
proof (state)
this:
A' = row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
have row_add_iterate_A': "row_add_iterate A' n i j $ i $ b = A' $ i $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' n i j $ i $ b = A' $ i $ b
[PROOF STEP]
using hyp Suc_n_less_card i_less_suc False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n < nrows ?A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ i $ b = ?A $ i $ b
Suc n < nrows A
mod_type_class.to_nat i \<le> Suc n
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. row_add_iterate A' n i j $ i $ b = A' $ i $ b
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n < CARD('m); mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ i $ b = ?A $ i $ b
Suc n < CARD('m)
mod_type_class.to_nat i \<le> Suc n
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. row_add_iterate A' n i j $ i $ b = A' $ i $ b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_add_iterate A' n i j $ i $ b = A' $ i $ b

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
have from_nat_noteq_i: "from_nat (Suc n) \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) \<noteq> i
[PROOF STEP]
using False Suc_n_less_card from_nat_not_eq
[PROOF STATE]
proof (prove)
using this:
Suc n \<noteq> mod_type_class.to_nat i
Suc n < nrows A
\<lbrakk>?a \<noteq> mod_type_class.to_nat ?b; ?a < CARD(?'a)\<rbrakk> \<Longrightarrow> mod_type_class.from_nat ?a \<noteq> ?b

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) \<noteq> i
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc n \<noteq> mod_type_class.to_nat i
Suc n < CARD('m)
\<lbrakk>?a \<noteq> mod_type_class.to_nat ?b; ?a < CARD(?'a)\<rbrakk> \<Longrightarrow> mod_type_class.from_nat ?a \<noteq> ?b

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) \<noteq> i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (Suc n) \<noteq> i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b
[PROOF STEP]
unfolding row_add_iterate.simps if_not_P[OF False] row_add_iterate_A'[unfolded A'_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ i $ b = A $ i $ b
[PROOF STEP]
unfolding row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ i $ b = A $ i $ b
[PROOF STEP]
using from_nat_noteq_i
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat (Suc n) \<noteq> i

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ i $ b = A $ i $ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ i $ b = A $ i $ b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_add_iterate_eq_row_add:
  fixes A::"'a::{ring_1}^'n^'m::{mod_type}"
  assumes a_not_i: "a \<noteq> i"
  and n: "n<nrows A"
  and "to_nat a \<le> n"
  shows "(row_add_iterate A n i j) $ a $ b = (row_add A a i (- A $ a $ j)) $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> i
n < nrows A
mod_type_class.to_nat a \<le> n

goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>a \<noteq> i; 0 < nrows A; mod_type_class.to_nat a \<le> 0\<rbrakk> \<Longrightarrow> row_add_iterate A 0 i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>a \<noteq> i; n < nrows A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b; a \<noteq> i; Suc n < nrows A; mod_type_class.to_nat a \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
a \<noteq> i
0 < nrows A
mod_type_class.to_nat a \<le> 0

goal (2 subgoals):
 1. \<And>A. \<lbrakk>a \<noteq> i; 0 < nrows A; mod_type_class.to_nat a \<le> 0\<rbrakk> \<Longrightarrow> row_add_iterate A 0 i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>a \<noteq> i; n < nrows A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b; a \<noteq> i; Suc n < nrows A; mod_type_class.to_nat a \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A 0 i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
unfolding row_add_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = (0::'m) then A else row_add A (0::'m) i (- A $ (0::'m) $ j)) $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
using "0.prems"(3) a_not_i to_nat_eq_0 least_mod_type
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a \<le> 0
a \<noteq> i
(mod_type_class.to_nat ?x = 0) = (?x = (0::?'a))
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. (if i = (0::'m) then A else row_add A (0::'m) i (- A $ (0::'m) $ j)) $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
row_add_iterate A 0 i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>a \<noteq> i; n < nrows A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b; a \<noteq> i; Suc n < nrows A; mod_type_class.to_nat a \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>a \<noteq> i; n < nrows A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b; a \<noteq> i; Suc n < nrows A; mod_type_class.to_nat a \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
fix n and A::"'a::{ring_1}^'n^'m::{mod_type}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>a \<noteq> i; n < nrows A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b; a \<noteq> i; Suc n < nrows A; mod_type_class.to_nat a \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
assume hyp: "(\<And>A::'a::{ring_1}^'n^'m::{mod_type}. a \<noteq> i \<Longrightarrow> n < nrows A  \<Longrightarrow> to_nat a \<le> n
    \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b)"
    and a_not_i: "a \<noteq> i"
    and suc_n_less_card: "Suc n < nrows A"
    and a_le_suc_n: "to_nat a \<le> Suc n"
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<noteq> i; n < nrows ?A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate ?A n i j $ a $ b = row_add ?A a i (- ?A $ a $ j) $ a $ b
a \<noteq> i
Suc n < nrows A
mod_type_class.to_nat a \<le> Suc n

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>a \<noteq> i; n < nrows A; mod_type_class.to_nat a \<le> n\<rbrakk> \<Longrightarrow> row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b; a \<noteq> i; Suc n < nrows A; mod_type_class.to_nat a \<le> Suc n\<rbrakk> \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
show "row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
proof (cases "Suc n = to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
show "row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
unfolding row_add_iterate.simps if_P[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
apply (rule hyp[OF a_not_i], auto simp add: Suc_lessD suc_n_less_card)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat a \<le> n
[PROOF STEP]
by (metis True a_le_suc_n a_not_i le_SucE to_nat_eq)
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
note Suc_n_not_i=False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
unfolding row_add_iterate.simps if_not_P[OF False]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
proof (cases "to_nat a = Suc n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat a = Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
 2. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat a = Suc n

goal (2 subgoals):
 1. mod_type_class.to_nat a = Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
 2. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
show "row_add_iterate (row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
by (metis Suc_le_lessD True order_refl less_imp_le row_add_iterate_preserves_greater_than_n suc_n_less_card to_nat_from_nat nrows_def)
[PROOF STATE]
proof (state)
this:
row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat a \<noteq> Suc n

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
define A' where "A' = row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)"
[PROOF STATE]
proof (state)
this:
A' = row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
have rw: "row_add_iterate A' n i j $ a $ b = row_add A' a i (- A' $ a $ j) $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' n i j $ a $ b = row_add A' a i (- A' $ a $ j) $ a $ b
[PROOF STEP]
proof (rule hyp)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a \<noteq> i
 2. n < nrows A'
 3. mod_type_class.to_nat a \<le> n
[PROOF STEP]
show "a \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> i
[PROOF STEP]
using a_not_i
[PROOF STATE]
proof (prove)
using this:
a \<noteq> i

goal (1 subgoal):
 1. a \<noteq> i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a \<noteq> i

goal (2 subgoals):
 1. n < nrows A'
 2. mod_type_class.to_nat a \<le> n
[PROOF STEP]
show "n < nrows A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < nrows A'
[PROOF STEP]
using suc_n_less_card
[PROOF STATE]
proof (prove)
using this:
Suc n < nrows A

goal (1 subgoal):
 1. n < nrows A'
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc n < CARD('m)

goal (1 subgoal):
 1. n < CARD('m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < nrows A'

goal (1 subgoal):
 1. mod_type_class.to_nat a \<le> n
[PROOF STEP]
show "to_nat a \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat a \<le> n
[PROOF STEP]
using False a_le_suc_n
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a \<noteq> Suc n
mod_type_class.to_nat a \<le> Suc n

goal (1 subgoal):
 1. mod_type_class.to_nat a \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat a \<le> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A' n i j $ a $ b = row_add A' a i (- A' $ a $ j) $ a $ b

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
have rw1: "row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j) $ a $ b = A $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ a $ b = A $ a $ b
[PROOF STEP]
unfolding row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ b = A $ a $ b
[PROOF STEP]
using False suc_n_less_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a \<noteq> Suc n
Suc n < nrows A

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ b = A $ a $ b
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a \<noteq> Suc n
Suc n < CARD('m)

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ b = A $ a $ b
[PROOF STEP]
by (auto simp add: to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ a $ b = A $ a $ b

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
have rw2: "row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j) $ a $ j = A $ a $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ a $ j = A $ a $ j
[PROOF STEP]
unfolding row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ j = A $ a $ j
[PROOF STEP]
using False suc_n_less_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a \<noteq> Suc n
Suc n < nrows A

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ j = A $ a $ j
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat a \<noteq> Suc n
Suc n < CARD('m)

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ a $ j = A $ a $ j
[PROOF STEP]
by (auto simp add: to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ a $ j = A $ a $ j

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
have rw3: "row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j) $ i $ b = A $ i $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ i $ b = A $ i $ b
[PROOF STEP]
unfolding row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ i $ b = A $ i $ b
[PROOF STEP]
using Suc_n_not_i suc_n_less_card
[PROOF STATE]
proof (prove)
using this:
Suc n \<noteq> mod_type_class.to_nat i
Suc n < nrows A

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ i $ b = A $ i $ b
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc n \<noteq> mod_type_class.to_nat i
Suc n < CARD('m)

goal (1 subgoal):
 1. (\<chi>ia ja. if ia = mod_type_class.from_nat (Suc n) then A $ mod_type_class.from_nat (Suc n) $ ja + - A $ mod_type_class.from_nat (Suc n) $ j * A $ i $ ja else A $ ia $ ja) $ i $ b = A $ i $ b
[PROOF STEP]
by (auto simp add: to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j) $ i $ b = A $ i $ b

goal (1 subgoal):
 1. mod_type_class.to_nat a \<noteq> Suc n \<Longrightarrow> row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
show  "row_add_iterate A' n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b
[PROOF STEP]
unfolding rw row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = a then A' $ a $ ja + - A' $ a $ j * A' $ i $ ja else A' $ ia $ ja) $ a $ b = (\<chi>ia ja. if ia = a then A $ a $ ja + - A $ a $ j * A $ i $ ja else A $ ia $ ja) $ a $ b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $ a $ b - A' $ a $ j * A' $ i $ b = A $ a $ b - A $ a $ j * A $ i $ b
[PROOF STEP]
unfolding A'_def rw1 rw2 rw3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ a $ b - A $ a $ j * A $ i $ b = A $ a $ b - A $ a $ j * A $ i $ b
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
row_add_iterate A' n i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A (Suc n) i j $ a $ b = row_add A a i (- A $ a $ j) $ a $ b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_add_iterate_eq_Gauss_Jordan_in_ij:
  fixes A::"'a::{field}^'n^'m::{mod_type}" and i::"'m" and j::"'n"
  defines A': "A'== mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) $ i $ j)"
  shows "row_add_iterate A' (nrows A - 1) i j = Gauss_Jordan_in_ij A i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' (nrows A - 1) i j = Gauss_Jordan_in_ij A i j
[PROOF STEP]
proof (unfold Gauss_Jordan_in_ij_def Let_def, vector, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) $ i $ ia
 2. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
fix ia
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) $ i $ ia
 2. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
have interchange_rw: "A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j
[PROOF STEP]
using interchange_rows_j[symmetric, of A "(LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)"]
[PROOF STATE]
proof (prove)
using this:
A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = interchange_rows A (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) ?j $ ?j

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j

goal (2 subgoals):
 1. \<And>ia. row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) $ i $ ia
 2. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
show "row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia =
    mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j) $ i $ ia"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) $ i $ ia
[PROOF STEP]
unfolding interchange_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ i $ ia
[PROOF STEP]
unfolding A'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ i $ ia
[PROOF STEP]
proof (rule row_add_iterate_preserves_pivot_row, unfold nrows_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. CARD('m) - Suc 0 < CARD('m)
 2. mod_type_class.to_nat i \<le> CARD('m) - Suc 0
[PROOF STEP]
show "CARD('m) - Suc 0 < CARD('m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('m) - Suc 0 < CARD('m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CARD('m) - Suc 0 < CARD('m)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<le> CARD('m) - Suc 0
[PROOF STEP]
have "to_nat i < CARD('m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i < CARD('m)
[PROOF STEP]
using bij_to_nat[where ?'a='m]
[PROOF STATE]
proof (prove)
using this:
bij_betw mod_type_class.to_nat UNIV {0..<CARD('m)}

goal (1 subgoal):
 1. mod_type_class.to_nat i < CARD('m)
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj mod_type_class.to_nat \<and> range mod_type_class.to_nat = {0..<CARD('m)}

goal (1 subgoal):
 1. mod_type_class.to_nat i < CARD('m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < CARD('m)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<le> CARD('m) - Suc 0
[PROOF STEP]
thus "to_nat i \<le> CARD('m) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < CARD('m)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<le> CARD('m) - Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i \<le> CARD('m) - Suc 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A' (nrows A - Suc 0) i j $ i $ ia = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) $ i $ ia

goal (1 subgoal):
 1. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
fix ia iaa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
have interchange_rw: "A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j
[PROOF STEP]
using interchange_rows_j[symmetric, of A "(LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)"]
[PROOF STATE]
proof (prove)
using this:
A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = interchange_rows A (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) ?j $ ?j

goal (1 subgoal):
 1. A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j = interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j

goal (1 subgoal):
 1. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
assume ia_not_i: "ia \<noteq> i"
[PROOF STATE]
proof (state)
this:
ia \<noteq> i

goal (1 subgoal):
 1. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
have rw: "(- interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ ia $ j)
    = - mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j) $ ia $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j = - mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ ia $ j
[PROOF STEP]
unfolding interchange_rows_def mult_row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ ia $ j = - (\<chi>ia ja. if ia = i then (1::'a) / (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ i $ j * (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ i $ ja else (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ ia $ ja) $ ia $ j
[PROOF STEP]
using ia_not_i
[PROOF STATE]
proof (prove)
using this:
ia \<noteq> i

goal (1 subgoal):
 1. - (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ ia $ j = - (\<chi>ia ja. if ia = i then (1::'a) / (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ i $ j * (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ i $ ja else (\<chi>ia ja. if ia = i then A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ja else if ia = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then A $ i $ ja else A $ ia $ ja) $ ia $ ja) $ ia $ j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j = - mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ ia $ j

goal (1 subgoal):
 1. \<And>ia iaa. ia \<noteq> i \<Longrightarrow> row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
show "row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa =
             row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j)) ia i
              (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ ia $ j) $
             ia $
             iaa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa
[PROOF STEP]
unfolding interchange_rw A' rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) ia i (- mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ ia $ j) $ ia $ iaa
[PROOF STEP]
proof (rule row_add_iterate_eq_row_add[of ia i "(nrows A - Suc 0)" _ j iaa], unfold nrows_def)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ia \<noteq> i
 2. CARD('m) - Suc 0 < CARD('m)
 3. mod_type_class.to_nat ia \<le> CARD('m) - Suc 0
[PROOF STEP]
show "ia \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia \<noteq> i
[PROOF STEP]
using ia_not_i
[PROOF STATE]
proof (prove)
using this:
ia \<noteq> i

goal (1 subgoal):
 1. ia \<noteq> i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ia \<noteq> i

goal (2 subgoals):
 1. CARD('m) - Suc 0 < CARD('m)
 2. mod_type_class.to_nat ia \<le> CARD('m) - Suc 0
[PROOF STEP]
show "CARD('m) - Suc 0 < CARD('m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('m) - Suc 0 < CARD('m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CARD('m) - Suc 0 < CARD('m)

goal (1 subgoal):
 1. mod_type_class.to_nat ia \<le> CARD('m) - Suc 0
[PROOF STEP]
have "to_nat ia < CARD('m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat ia < CARD('m)
[PROOF STEP]
using bij_to_nat[where ?'a='m]
[PROOF STATE]
proof (prove)
using this:
bij_betw mod_type_class.to_nat UNIV {0..<CARD('m)}

goal (1 subgoal):
 1. mod_type_class.to_nat ia < CARD('m)
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj mod_type_class.to_nat \<and> range mod_type_class.to_nat = {0..<CARD('m)}

goal (1 subgoal):
 1. mod_type_class.to_nat ia < CARD('m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ia < CARD('m)

goal (1 subgoal):
 1. mod_type_class.to_nat ia \<le> CARD('m) - Suc 0
[PROOF STEP]
thus "to_nat ia \<le> CARD('m) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ia < CARD('m)

goal (1 subgoal):
 1. mod_type_class.to_nat ia \<le> CARD('m) - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ia \<le> CARD('m) - Suc 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_add_iterate A' (nrows A - Suc 0) i j $ ia $ iaa = row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j)) ia i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ ia $ j) $ ia $ iaa

goal:
No subgoals!
[PROOF STEP]
qed