[STATEMENT]
lemma foldl_Gauss_condition_3:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes k: "k < ncols A"
  and all_zero: "\<forall>m. is_zero_row_upt_k m k A"
  and Amk_not_zero: "A $ m $ from_nat k \<noteq> 0"
  and "\<not> is_zero_row_upt_k ma (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))"
  shows "to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))) = 0
[PROOF STEP]
proof (unfold to_nat_eq_0, rule Greatest_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
 2. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
have to_nat_from_nat_k_suc: "to_nat (from_nat k::'columns) < Suc (k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
using to_nat_from_nat_id[OF k[unfolded ncols_def]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat k) = k

goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

goal (2 subgoals):
 1. \<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
 2. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
have A0k_eq_1: "(Gauss_Jordan_in_ij A 0 (from_nat k)) $ 0 $ (from_nat k) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
by (rule Gauss_Jordan_in_ij_1, auto intro!: Amk_not_zero least_mod_type)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k = (1::'a)

goal (2 subgoals):
 1. \<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
 2. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
show "\<not> is_zero_row_upt_k 0 (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ j = (0::'a))
[PROOF STEP]
using A0k_eq_1 to_nat_from_nat_k_suc
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ mod_type_class.from_nat k = (1::'a)
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ (0::'rows) $ j = (0::'a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (0::'rows) (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
assume not_zero_y: "\<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
have y_eq_0: "y=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = (0::'rows)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
assume y_not_0: "y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
y \<noteq> (0::'rows)

goal (1 subgoal):
 1. y \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
have "is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A 0 (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
fix j::"'columns"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
assume j: "to_nat j < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < Suc k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A 0 (from_nat k) $ y $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
proof (cases "to_nat j = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat j = k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
 2. mod_type_class.to_nat j \<noteq> k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = k

goal (2 subgoals):
 1. mod_type_class.to_nat j = k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
 2. mod_type_class.to_nat j \<noteq> k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
unfolding to_nat_from_nat[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) j $ y $ j = (0::'a)
[PROOF STEP]
by (rule Gauss_Jordan_in_ij_0[OF _ y_not_0], unfold to_nat_from_nat[OF True, symmetric], auto intro!:  y_not_0 least_mod_type Amk_not_zero)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal (1 subgoal):
 1. mod_type_class.to_nat j \<noteq> k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat j \<noteq> k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j \<noteq> k

goal (1 subgoal):
 1. mod_type_class.to_nat j \<noteq> k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
hence j_less_k: "to_nat j < k"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j \<noteq> k

goal (1 subgoal):
 1. mod_type_class.to_nat j < k
[PROOF STEP]
by (metis j less_SucE)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. mod_type_class.to_nat j \<noteq> k \<Longrightarrow> Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero j_less_k Amk_not_zero]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ j = A $ ?i $ j

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
using all_zero j_less_k
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ j = A $ ?i $ j
\<forall>m. is_zero_row_upt_k m k A
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ ?i $ j = A $ ?i $ j
\<forall>m j. mod_type_class.to_nat j < k \<longrightarrow> A $ m $ j = (0::'a)
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. y \<noteq> (0::'rows) \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. False
[PROOF STEP]
using not_zero_y
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))
\<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y = (0::'rows)

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A (0::'rows) (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> (0::'rows)
[PROOF STEP]
thus "y\<le>0"
[PROOF STATE]
proof (prove)
using this:
y = (0::'rows)

goal (1 subgoal):
 1. y \<le> (0::'rows)
[PROOF STEP]
using least_mod_type
[PROOF STATE]
proof (prove)
using this:
y = (0::'rows)
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. y \<le> (0::'rows)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<le> (0::'rows)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_Gauss_condition_5:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes rref_A: "reduced_row_echelon_form_upt_k A k"
  and not_zero_a:"\<not> is_zero_row_upt_k a k A"
  and all_zero_below_greatest: "\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
  shows "(GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)
[PROOF STEP]
have "\<And>n. (is_zero_row_upt_k n (Suc k) A) = (is_zero_row_upt_k n k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n (Suc k) A = is_zero_row_upt_k n k A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. is_zero_row_upt_k n (Suc k) A \<Longrightarrow> is_zero_row_upt_k n k A
 2. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. is_zero_row_upt_k n (Suc k) A \<Longrightarrow> is_zero_row_upt_k n k A
 2. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
assume "is_zero_row_upt_k n (Suc k) A"
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k n (Suc k) A

goal (2 subgoals):
 1. \<And>n. is_zero_row_upt_k n (Suc k) A \<Longrightarrow> is_zero_row_upt_k n k A
 2. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
thus "is_zero_row_upt_k n k A"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k n (Suc k) A

goal (1 subgoal):
 1. is_zero_row_upt_k n k A
[PROOF STEP]
using is_zero_row_upt_k_le
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k n (Suc k) A
is_zero_row_upt_k ?i (Suc ?k) ?A \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A

goal (1 subgoal):
 1. is_zero_row_upt_k n k A
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k n k A

goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
assume zero_n_k: "is_zero_row_upt_k n k A"
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k n k A

goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
have "n>(GREATEST n. \<not> is_zero_row_upt_k n k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) < n
[PROOF STEP]
by (rule greatest_less_zero_row[OF rref_A zero_n_k], auto intro!: not_zero_a)
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < n

goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
hence n_ge_gratest: "n \<ge> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < n

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
using le_Suc
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < n
?a < ?b \<Longrightarrow> ?a + (1::?'a) \<le> ?b

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
hence A_nk_zero: "A $ n $ (from_nat k) = 0"
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. A $ n $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
using all_zero_below_greatest
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. A $ n $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A $ n $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. \<And>n. is_zero_row_upt_k n k A \<Longrightarrow> is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
show "is_zero_row_upt_k n (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k n (Suc k) A
[PROOF STEP]
by (rule is_zero_row_upt_k_suc[OF zero_n_k A_nk_zero])
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k n (Suc k) A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k ?n (Suc k) A = is_zero_row_upt_k ?n k A

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)
[PROOF STEP]
thus "(GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k ?n (Suc k) A = is_zero_row_upt_k ?n k A

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_Gauss_condition_6:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and eq_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A"
  shows "nrows A = Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
have "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
using greatest_plus_one_eq_0[OF eq_card]
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)

goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
hence greatest_k_eq_minus_1: "(GREATEST n. \<not> is_zero_row_upt_k n k A) = -1"
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)
[PROOF STEP]
using a_eq_minus_1
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
\<forall>a. a + (1::?'a) = (0::?'a) \<longrightarrow> a = - (1::?'a)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)

goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
have "(GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A) = - (1::'rows)
[PROOF STEP]
proof (rule Greatest_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row_upt_k (- (1::'rows)) (Suc k) A
 2. \<And>y. \<not> is_zero_row_upt_k y (Suc k) A \<Longrightarrow> y \<le> - (1::'rows)
[PROOF STEP]
show "\<not> is_zero_row_upt_k (- 1) (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (- (1::'rows)) (Suc k) A
[PROOF STEP]
using GreatestI_ex greatest_k_eq_minus_1 is_zero_row_upt_k_le not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<exists>x. ?P x \<Longrightarrow> ?P (Greatest ?P)
(GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)
is_zero_row_upt_k ?i (Suc ?k) ?A \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (- (1::'rows)) (Suc k) A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (- (1::'rows)) (Suc k) A

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) A \<Longrightarrow> y \<le> - (1::'rows)
[PROOF STEP]
show "\<And>y. \<not> is_zero_row_upt_k y (Suc k) A \<Longrightarrow> y \<le> -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) A \<Longrightarrow> y \<le> - (1::'rows)
[PROOF STEP]
using Greatest_is_minus_1
[PROOF STATE]
proof (prove)
using this:
\<forall>a. a \<le> - (1::?'a)

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) A \<Longrightarrow> y \<le> - (1::'rows)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k ?y (Suc k) A \<Longrightarrow> ?y \<le> - (1::'rows)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A) = - (1::'rows)

goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
thus "nrows A = Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))"
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A) = - (1::'rows)

goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
using eq_card greatest_k_eq_minus_1
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A) = - (1::'rows)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A
(GREATEST n. \<not> is_zero_row_upt_k n k A) = - (1::'rows)

goal (1 subgoal):
 1. nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
nrows A = Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_Gauss_condition_8:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes k: "k < ncols A"
  and not_zero_m: " \<not> is_zero_row_upt_k m k A"
  and A_ma_k: " A $ ma $ from_nat k \<noteq> 0"
  and ma: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> ma"
  shows "\<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
define Greatest_plus_one where "Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (state)
this:
Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
have to_nat_from_nat_k_suc: "to_nat (from_nat k::'columns) < (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
using to_nat_from_nat_id[OF k[unfolded ncols_def]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat k) = k

goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
have Gauss_eq_1: "(Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k)) $ Greatest_plus_one $ (from_nat k) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
by (unfold Greatest_plus_one_def, rule Gauss_Jordan_in_ij_1, auto intro!: A_ma_k ma)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)

goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
show "\<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A (Greatest_plus_one) (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
[PROOF STEP]
by (rule exI[of _ "Greatest_plus_one"], unfold is_zero_row_upt_k_def, auto, rule exI[of _ "from_nat k"], simp add: Gauss_eq_1 to_nat_from_nat_k_suc)
[PROOF STATE]
proof (state)
this:
\<exists>m. \<not> is_zero_row_upt_k m (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldl_Gauss_condition_9:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes k: "k < ncols A"
  and rref_A: "reduced_row_echelon_form_upt_k A k"
  assumes not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and suc_greatest_not_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A"
  and greatest_less_ma: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> ma"
  and A_ma_k: "A $ ma $ from_nat k \<noteq> 0"
  shows "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) =
  to_nat(GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
define Greatest_plus_one where "Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (state)
this:
Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
have to_nat_from_nat_k_suc: "to_nat (from_nat k::'columns) < (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
using to_nat_from_nat_id[OF k[unfolded ncols_def]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat k) = k

goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
have greatest_plus_one_not_zero: "Greatest_plus_one \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Greatest_plus_one \<noteq> (0::'rows)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Greatest_plus_one \<noteq> (0::'rows)
[PROOF STEP]
have "to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < nrows A
[PROOF STEP]
using to_nat_less_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?j < CARD(?'a)

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?j < CARD(?'a)

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < CARD('rows)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < nrows A

goal (1 subgoal):
 1. Greatest_plus_one \<noteq> (0::'rows)
[PROOF STEP]
hence "to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < nrows A"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < nrows A

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < nrows A
[PROOF STEP]
using suc_greatest_not_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) < nrows A
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < nrows A
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 < nrows A

goal (1 subgoal):
 1. Greatest_plus_one \<noteq> (0::'rows)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Greatest_plus_one \<noteq> (0::'rows)
[PROOF STEP]
unfolding Greatest_plus_one_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
by (rule suc_not_zero[OF suc_greatest_not_card[unfolded Suc_eq_plus1 nrows_def]])
[PROOF STATE]
proof (state)
this:
Greatest_plus_one \<noteq> (0::'rows)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Greatest_plus_one \<noteq> (0::'rows)

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
have greatest_eq: "Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)))
[PROOF STEP]
proof (rule Greatest_equality[symmetric])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row_upt_k Greatest_plus_one (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
 2. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
have "(Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k)) $ (Greatest_plus_one) $ (from_nat k) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
by (unfold Greatest_plus_one_def, rule Gauss_Jordan_in_ij_1, auto intro!: greatest_less_ma A_ma_k)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)

goal (2 subgoals):
 1. \<not> is_zero_row_upt_k Greatest_plus_one (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
 2. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
thus "\<not> is_zero_row_upt_k Greatest_plus_one (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k))"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k Greatest_plus_one (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
[PROOF STEP]
using to_nat_from_nat_k_suc
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k Greatest_plus_one (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ mod_type_class.from_nat k = (1::'a)
mod_type_class.to_nat (mod_type_class.from_nat k) < Suc k

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ Greatest_plus_one $ j = (0::'a))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k Greatest_plus_one (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
assume not_zero_y: "\<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k))"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))

goal (1 subgoal):
 1. \<And>y. \<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)) \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
show "y \<le> Greatest_plus_one"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> Greatest_plus_one
[PROOF STEP]
proof (cases "y<Greatest_plus_one")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
 2. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y < Greatest_plus_one

goal (2 subgoals):
 1. y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
 2. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y < Greatest_plus_one

goal (1 subgoal):
 1. y \<le> Greatest_plus_one
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<le> Greatest_plus_one

goal (1 subgoal):
 1. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> y < Greatest_plus_one

goal (1 subgoal):
 1. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
hence y_ge_greatest: "y\<ge>Greatest_plus_one"
[PROOF STATE]
proof (prove)
using this:
\<not> y < Greatest_plus_one

goal (1 subgoal):
 1. Greatest_plus_one \<le> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Greatest_plus_one \<le> y

goal (1 subgoal):
 1. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
have "y=Greatest_plus_one"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = Greatest_plus_one
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> Greatest_plus_one \<Longrightarrow> False
[PROOF STEP]
assume y_not_greatest: "y \<noteq> Greatest_plus_one"
[PROOF STATE]
proof (state)
this:
y \<noteq> Greatest_plus_one

goal (1 subgoal):
 1. y \<noteq> Greatest_plus_one \<Longrightarrow> False
[PROOF STEP]
have "(GREATEST n. \<not> is_zero_row_upt_k n k A) < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) < y
[PROOF STEP]
using greatest_plus_one_not_zero
[PROOF STATE]
proof (prove)
using this:
Greatest_plus_one \<noteq> (0::'rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) < y
[PROOF STEP]
using Suc_le' less_le_trans y_ge_greatest
[PROOF STATE]
proof (prove)
using this:
Greatest_plus_one \<noteq> (0::'rows)
?a + (1::?'a) \<noteq> (0::?'a) \<Longrightarrow> ?a < ?a + (1::?'a)
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
Greatest_plus_one \<le> y

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) < y
[PROOF STEP]
unfolding Greatest_plus_one_def
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
?a + (1::?'a) \<noteq> (0::?'a) \<Longrightarrow> ?a < ?a + (1::?'a)
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> y

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) < y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < y

goal (1 subgoal):
 1. y \<noteq> Greatest_plus_one \<Longrightarrow> False
[PROOF STEP]
hence zero_row_y_upt_k: "is_zero_row_upt_k y k A"
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < y

goal (1 subgoal):
 1. is_zero_row_upt_k y k A
[PROOF STEP]
using not_greater_Greatest[of "\<lambda>n. \<not> is_zero_row_upt_k n k A" y]
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < y
(GREATEST x. \<not> is_zero_row_upt_k x k A) < y \<Longrightarrow> \<not> \<not> is_zero_row_upt_k y k A

goal (1 subgoal):
 1. is_zero_row_upt_k y k A
[PROOF STEP]
unfolding Greatest_plus_one_def
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) < y
(GREATEST x. \<not> is_zero_row_upt_k x k A) < y \<Longrightarrow> \<not> \<not> is_zero_row_upt_k y k A

goal (1 subgoal):
 1. is_zero_row_upt_k y k A
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k y k A

goal (1 subgoal):
 1. y \<noteq> Greatest_plus_one \<Longrightarrow> False
[PROOF STEP]
have "is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
fix j::'columns
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
assume j: "to_nat j < Suc k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < Suc k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k) $ y $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
proof (cases "j=from_nat k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
 2. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j = mod_type_class.from_nat k

goal (2 subgoals):
 1. j = mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
 2. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
proof (unfold True, rule Gauss_Jordan_in_ij_0[OF _ y_not_greatest], rule exI[of _ ma], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. Greatest_plus_one \<le> ma
[PROOF STEP]
show "A $ ma $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using A_ma_k
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. Greatest_plus_one \<le> ma
[PROOF STEP]
show "Greatest_plus_one \<le> ma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Greatest_plus_one \<le> ma
[PROOF STEP]
using greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. Greatest_plus_one \<le> ma
[PROOF STEP]
unfolding Greatest_plus_one_def
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Greatest_plus_one \<le> ma

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
j \<noteq> mod_type_class.from_nat k

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
hence j_le_suc_k: "to_nat j < Suc k"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> mod_type_class.from_nat k

goal (1 subgoal):
 1. mod_type_class.to_nat j < Suc k
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j \<noteq> mod_type_class.from_nat k
mod_type_class.to_nat j < Suc k

goal (1 subgoal):
 1. mod_type_class.to_nat j < Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < Suc k

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
have "Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k) $ y $ j = A $ y $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = A $ y $ j
[PROOF STEP]
unfolding Greatest_plus_one_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ y $ j = A $ y $ j
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_preserves_previous_elements)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. reduced_row_echelon_form_upt_k A k
 2. \<not> is_zero_row_upt_k ?a k A
 3. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 4. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 5. mod_type_class.to_nat j < k
[PROOF STEP]
show "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
using rref_A
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A k

goal (4 subgoals):
 1. \<not> is_zero_row_upt_k ?a k A
 2. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 3. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 4. mod_type_class.to_nat j < k
[PROOF STEP]
show "\<not> is_zero_row_upt_k m k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k m k A
[PROOF STEP]
using not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k m k A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k m k A

goal (3 subgoals):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 2. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 3. mod_type_class.to_nat j < k
[PROOF STEP]
show "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
using A_ma_k greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n

goal (2 subgoals):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
 2. mod_type_class.to_nat j < k
[PROOF STEP]
show "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
using greatest_plus_one_not_zero
[PROOF STATE]
proof (prove)
using this:
Greatest_plus_one \<noteq> (0::'rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
unfolding Greatest_plus_one_def
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)

goal (1 subgoal):
 1. mod_type_class.to_nat j < k
[PROOF STEP]
show "to_nat j < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat j < k
[PROOF STEP]
using False from_nat_to_nat_id j_le_suc_k less_antisym
[PROOF STATE]
proof (prove)
using this:
j \<noteq> mod_type_class.from_nat k
mod_type_class.from_nat (mod_type_class.to_nat ?x) = ?x
mod_type_class.to_nat j < Suc k
\<lbrakk>\<not> ?n < ?m; ?n < Suc ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. mod_type_class.to_nat j < k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = A $ y $ j

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = A $ y $ j

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ y $ j = (0::'a)
[PROOF STEP]
using zero_row_y_upt_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k y k A

goal (1 subgoal):
 1. A $ y $ j = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ y $ j = (0::'a)

goal (1 subgoal):
 1. A $ y $ j = (0::'a)
[PROOF STEP]
using  False le_imp_less_or_eq from_nat_to_nat_id j_le_suc_k less_Suc_eq_le
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ y $ j = (0::'a)
j \<noteq> mod_type_class.from_nat k
?x \<le> ?y \<Longrightarrow> ?x < ?y \<or> ?x = ?y
mod_type_class.from_nat (mod_type_class.to_nat ?x) = ?x
mod_type_class.to_nat j < Suc k
(?m < Suc ?n) = (?m \<le> ?n)

goal (1 subgoal):
 1. A $ y $ j = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ y $ j = (0::'a)

goal (1 subgoal):
 1. j \<noteq> mod_type_class.from_nat k \<Longrightarrow> Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
show "Gauss_Jordan_in_ij A Greatest_plus_one (from_nat k) $ y $ j = 0"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k) $ y $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))

goal (1 subgoal):
 1. y \<noteq> Greatest_plus_one \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))

goal (1 subgoal):
 1. False
[PROOF STEP]
using not_zero_y
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))
\<not> is_zero_row_upt_k y (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y = Greatest_plus_one

goal (1 subgoal):
 1. \<not> y < Greatest_plus_one \<Longrightarrow> y \<le> Greatest_plus_one
[PROOF STEP]
thus "y \<le> Greatest_plus_one"
[PROOF STATE]
proof (prove)
using this:
y = Greatest_plus_one

goal (1 subgoal):
 1. y \<le> Greatest_plus_one
[PROOF STEP]
using y_ge_greatest
[PROOF STATE]
proof (prove)
using this:
y = Greatest_plus_one
Greatest_plus_one \<le> y

goal (1 subgoal):
 1. y \<le> Greatest_plus_one
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<le> Greatest_plus_one

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<le> Greatest_plus_one

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Greatest_plus_one = (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A Greatest_plus_one (mod_type_class.from_nat k)))

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
show "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) =
    to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))
[PROOF STEP]
unfolding greatest_eq[unfolded Greatest_plus_one_def, symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows))
[PROOF STEP]
unfolding add_to_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + mod_type_class.to_nat (1::'rows)))
[PROOF STEP]
unfolding to_nat_1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1))
[PROOF STEP]
using to_nat_from_nat_id to_nat_plus_one_less_card
[PROOF STATE]
proof (prove)
using this:
?x < CARD(?'a) \<Longrightarrow> mod_type_class.to_nat (mod_type_class.from_nat ?x) = ?x
\<forall>a. a + (1::?'a) \<noteq> (0::?'a) \<longrightarrow> mod_type_class.to_nat a + 1 < CARD(?'a)

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1))
[PROOF STEP]
using greatest_plus_one_not_zero[unfolded Greatest_plus_one_def]
[PROOF STATE]
proof (prove)
using this:
?x < CARD(?'a) \<Longrightarrow> mod_type_class.to_nat (mod_type_class.from_nat ?x) = ?x
\<forall>a. a + (1::?'a) \<noteq> (0::?'a) \<longrightarrow> mod_type_class.to_nat a + 1 < CARD(?'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)))

goal:
No subgoals!
[PROOF STEP]
qed