[STATEMENT]
lemma condition_3_part_5:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia\<equiv>(if \<forall>m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
  defines B:"B\<equiv>(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and i_le: "i < i + 1"
  and not_zero_i_suc_k: "\<not> is_zero_row_upt_k i (Suc k) B"
  and not_zero_suc_i_suc_k: "\<not> is_zero_row_upt_k (i + 1) (Suc k) B"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and 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_not_zero: "A $ ma $ from_nat k \<noteq> 0"
  shows "(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n \<noteq> 0)
  < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have ia2: "ia=to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
unfolding ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<forall>m. is_zero_row_upt_k m k A then 0 else mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[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. (if \<forall>m. is_zero_row_upt_k m k A then 0 else mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have B_eq_Gauss: "B = 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. B = 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 B Gauss_Jordan_column_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let i = fst (ia, A); A = snd (ia, A); from_nat_i = mod_type_class.from_nat i; from_nat_k = mod_type_class.from_nat k in if (\<forall>m\<ge>from_nat_i. A $ m $ from_nat_k = (0::'a)) \<or> i = nrows A then (i, A) else (i + 1, Gauss_Jordan_in_ij A from_nat_i from_nat_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 ia2 Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat 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]
using greatest_not_card greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat 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]
by (auto simp add: from_nat_to_nat_greatest)
[PROOF STATE]
proof (state)
this:
B = 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 (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have suc_greatest_not_zero: "(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 Suc_eq_plus1 suc_not_zero greatest_not_card
[PROOF STATE]
proof (prove)
using this:
Suc ?n = ?n + 1
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'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. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc ?n = ?n + 1
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> CARD('rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
by auto
[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. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
proof (cases "is_zero_row_upt_k (i + 1) k A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (i + (1::'rows)) k A

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have zero_i_plus_one_k_B: "is_zero_row_upt_k (i+1) k B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k (i + (1::'rows)) k B
[PROOF STEP]
by (unfold B_eq_Gauss, rule is_zero_after_Gauss[OF True not_zero_m rref greatest_less_ma A_ma_k_not_zero])
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (i + (1::'rows)) k B

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
hence Gauss_Jordan_i_not_0: "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ (from_nat k) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (i + (1::'rows)) k B

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) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using not_zero_suc_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (i + (1::'rows)) k B
\<not> is_zero_row_upt_k (i + (1::'rows)) (Suc k) B

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) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
unfolding B_eq_Gauss
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (i + (1::'rows)) 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))
\<not> is_zero_row_upt_k (i + (1::'rows)) (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 (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) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using is_zero_row_upt_k_suc
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (i + (1::'rows)) 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))
\<not> is_zero_row_upt_k (i + (1::'rows)) (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))
\<lbrakk>is_zero_row_upt_k ?i ?k ?A; ?A $ ?i $ mod_type_class.from_nat ?k = (0::?'b)\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?i (Suc ?k) ?A

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) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have i_plus_one_eq: "i + 1 = ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + (1::'rows) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
assume i_not_greatest: "i + 1 \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (state)
this:
i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
have "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i + 1) $ (from_nat k) = 0"
[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) $ (i + (1::'rows)) $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_0)
[PROOF STATE]
proof (state)
goal (2 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. i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[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 greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

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 (1 subgoal):
 1. i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
show "i + 1 \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
using i_not_greatest
[PROOF STATE]
proof (prove)
using this:
i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. i + (1::'rows) \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Gauss_Jordan_i_not_0
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ mod_type_class.from_nat k = (0::'a)
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)

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:
i + (1::'rows) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
hence i_eq_greatest: "i=(GREATEST n. \<not> is_zero_row_upt_k n k A)"
[PROOF STATE]
proof (prove)
using this:
i + (1::'rows) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

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

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

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have Least_eq_k: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ ka \<noteq> 0) = from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) = mod_type_class.from_nat k
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 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) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ from_nat k \<noteq> 0"
[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) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by (metis Gauss_Jordan_i_not_0)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
assume "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
thus "from_nat k \<le> y"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> y
[PROOF STEP]
using zero_i_plus_one_k_B
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)
is_zero_row_upt_k (i + (1::'rows)) k B

goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> y
[PROOF STEP]
unfolding i_eq_greatest B_eq_Gauss
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) $ y \<noteq> (0::'a)
is_zero_row_upt_k ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) 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 (1 subgoal):
 1. mod_type_class.from_nat k \<le> y
[PROOF STEP]
by (metis is_zero_row_upt_k_def not_less to_nat_le)
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) = mod_type_class.from_nat k

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have not_zero_i_A: "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using greatest_less_zero_row[OF rref] not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_zero_row_upt_k ?i k A; \<not> (\<forall>a. is_zero_row_upt_k a k A)\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
unfolding i_eq_greatest
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_zero_row_upt_k ?i k A; \<not> (\<forall>a. is_zero_row_upt_k a k A)\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k A) < ?i
\<not> is_zero_row_upt_k m k A

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

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> is_zero_row_upt_k i k A
[PROOF STEP]
obtain j where Aij_not_0: "A $ i $ j \<noteq> 0" and j_le_k: "to_nat j < k"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a))

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ i $ j \<noteq> (0::'a)
mod_type_class.to_nat j < k

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have least_le_k: "to_nat (LEAST ka. A $ i $ ka \<noteq> 0) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
[PROOF STEP]
by (metis (lifting, mono_tags) Aij_not_0 j_le_k less_trans linorder_cases not_less_Least to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have Least_eq: " (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n \<noteq> 0) =
      (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 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) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)) \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> 0) \<noteq> 0"
[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) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_i_A _ suc_greatest_not_zero least_le_k] greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

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) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref] not_zero_i_A
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row_upt_k i k A

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) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
assume Gauss_Jordan_y:"Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "(LEAST ka. A $ i $ ka \<noteq> 0) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
proof (cases "to_nat y < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat y < k

goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat y < k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by (metis not_le least_le_k less_trans to_nat_mono)
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat y < k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
have "A $ i $ y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_y
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ suc_greatest_not_zero True]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y
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. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
using Least_le
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have "... < from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < mod_type_class.from_nat k
[PROOF STEP]
by (metis is_zero_row_upt_k_def is_zero_row_upt_k_suc le_less_linear le_less_trans least_le_k not_zero_suc_i_suc_k to_nat_mono' zero_i_plus_one_k_B)
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < mod_type_class.from_nat k

goal (2 subgoals):
 1. is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 2. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < mod_type_class.from_nat k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < mod_type_class.from_nat k

goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding Least_eq_k
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < mod_type_class.from_nat k

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

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (i + (1::'rows)) k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have not_zero_i_A: "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using rref_upt_condition1[OF rref] False i_le
[PROOF STATE]
proof (prove)
using this:
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
\<not> is_zero_row_upt_k (i + (1::'rows)) k A
i < i + (1::'rows)

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

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> is_zero_row_upt_k i k A
[PROOF STEP]
obtain j where Aij_not_0: "A $ i $ j \<noteq> 0" and j_le_k: "to_nat j < k"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a))

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ i $ j \<noteq> (0::'a)
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have least_le_k: "to_nat (LEAST ka. A $ i $ ka \<noteq> 0) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
[PROOF STEP]
by (metis (lifting, mono_tags) Aij_not_0 j_le_k less_trans linorder_cases not_less_Least to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have Least_i_eq: "(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n \<noteq> 0)
      = (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 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) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)) \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> 0) \<noteq> 0"
[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) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_i_A _ suc_greatest_not_zero least_le_k] greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

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) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref] not_zero_i_A
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a))
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row_upt_k i k A

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) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
assume Gauss_Jordan_y:"Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "(LEAST ka. A $ i $ ka \<noteq> 0) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
proof (cases "to_nat y < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat y < k

goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat y < k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by (metis not_le not_less_iff_gr_or_eq le_less_trans least_le_k to_nat_mono)
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat y < k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
have "A $ i $ y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_y
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ suc_greatest_not_zero True]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y
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. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
using Least_le
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> is_zero_row_upt_k (i + (1::'rows)) k A
[PROOF STEP]
obtain s where Ais_not_0: "A $ (i+1) $ s \<noteq> 0" and s_le_k: "to_nat s < k"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k (i + (1::'rows)) k A

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>A $ (i + (1::'rows)) $ s \<noteq> (0::'a); mod_type_class.to_nat s < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ (i + (1::'rows)) $ j = (0::'a))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>A $ (i + (1::'rows)) $ s \<noteq> (0::'a); mod_type_class.to_nat s < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ (i + (1::'rows)) $ s \<noteq> (0::'a)
mod_type_class.to_nat s < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have least_le_k: "to_nat (LEAST ka. A $ (i+1) $ ka \<noteq> 0) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) < k
[PROOF STEP]
by (metis (lifting, mono_tags) Ais_not_0 s_le_k neq_iff less_trans not_less_Least to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
have Least_i_plus_one_eq: "(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ n \<noteq> 0)
      = (LEAST n. A $ (i+1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a)) = (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 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) $ (i + (1::'rows)) $ (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a)) \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ (LEAST ka. A $ (i+1) $ ka \<noteq> 0) \<noteq> 0"
[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) $ (i + (1::'rows)) $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_i_A _ suc_greatest_not_zero least_le_k] greatest_less_ma A_ma_k_not_zero
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a))
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)

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) $ (i + (1::'rows)) $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref] False
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) = A $ ?i $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a))
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row_upt_k (i + (1::'rows)) k A

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) $ (i + (1::'rows)) $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
assume Gauss_Jordan_y:"Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "(LEAST ka. A $ (i+1) $ ka \<noteq> 0) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
proof (cases "to_nat y < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat y < k

goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat y < k

goal (1 subgoal):
 1. (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by (metis (mono_tags) le_less_linear least_le_k less_trans to_nat_mono)
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat y < k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
have "A $ (i+1) $ y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (i + (1::'rows)) $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_y
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ (i + (1::'rows)) $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ suc_greatest_not_zero True]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y

goal (1 subgoal):
 1. A $ (i + (1::'rows)) $ y \<noteq> (0::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y
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. A $ (i + (1::'rows)) $ y \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ (i + (1::'rows)) $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $ (i + (1::'rows)) $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
using Least_le
[PROOF STATE]
proof (prove)
using this:
A $ (i + (1::'rows)) $ y \<noteq> (0::'a)
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. (LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ (i + (1::'rows)) $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a)) = (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<Longrightarrow> (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding Least_i_plus_one_eq Least_i_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using rref_upt_condition3[OF rref] i_le False not_zero_i_A
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
i < i + (1::'rows)
\<not> is_zero_row_upt_k (i + (1::'rows)) k A
\<not> is_zero_row_upt_k i k A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed