[STATEMENT]
lemma foldl_Gauss_Jordan_column_k_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows det_fst_Gauss_Jordan_upt_k_PA_eq_fst_Gauss_Jordan_upt_k_det_P: "fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))"
and snd_Gauss_Jordan_upt_k_det_P_is_snd_Gauss_Jordan_upt_k_PA: "snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)"
and fst_snd_foldl_Gauss_det_P_PA: "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)) &&& snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k) &&& fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))
 2. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
 3. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 5. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 6. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (6 subgoals):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))
 2. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
 3. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 5. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 6. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]))) = det (fst (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]), snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))))
[PROOF STEP]
by (simp, metis det_fst_Gauss_Jordan_column_k_PA_eq_fst_Gauss_Jordan_column_k_det_P det_I)
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A 0) = det (fst (Gauss_Jordan_upt_k_PA A 0))

goal (5 subgoals):
 1. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
 2. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 5. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = snd (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
using snd_Gauss_Jordan_column_k_det_P_is_snd_Gauss_Jordan_column_k_PA
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_column_k_det_P (?n, ?i, ?A) ?k) = snd (Gauss_Jordan_column_k_PA (?P, ?i, ?A) ?k)

goal (1 subgoal):
 1. snd (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = snd (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
snd (Gauss_Jordan_upt_k_det_P A 0) = snd (Gauss_Jordan_upt_k_PA A 0)

goal (4 subgoals):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 4. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc 0]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
using [[unfold_abs_def = false]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
unfolding Gauss_Jordan_column_k_det_P_def Gauss_Jordan_column_k_PA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = fst (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
using fst_snd_Gauss_Jordan_column_k_det_P_eq_fst_snd_Gauss_Jordan_column_k_PA
[PROOF STATE]
proof (prove)
using this:
fst (snd (Gauss_Jordan_column_k_det_P (?n, ?i, ?A) ?k)) = fst (snd (Gauss_Jordan_column_k_PA (?P, ?i, ?A) ?k))

goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (1::'a, 0, A) 0)) = fst (snd (Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) 0))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc 0]))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
assume hyp1: "fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))"
and hyp2: "snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)"
and hyp3: "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]))"
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))
snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have list_rw: "[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have det_mat_nn: "det (mat 1::'a^'n::{mod_type}^'n::{mod_type}) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat (1::'a)) = (1::'a)
[PROOF STEP]
using det_I
[PROOF STATE]
proof (prove)
using this:
det (mat (1::?'a)) = (1::?'a)

goal (1 subgoal):
 1. det (mat (1::'a)) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (mat (1::'a)) = (1::'a)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
define f where "f = foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k]"
[PROOF STATE]
proof (state)
this:
f = foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
define g where "g = foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]"
[PROOF STATE]
proof (state)
this:
g = foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have f_rw: "f = (fst f, fst (snd f), snd(snd f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = (fst f, fst (snd f), snd (snd f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = (fst f, fst (snd f), snd (snd f))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have g_rw: "g = (fst g, fst (snd g), snd(snd g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = (fst g, fst (snd g), snd (snd g))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g = (fst g, fst (snd g), snd (snd g))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have fst_snd: "fst (snd f) = fst (snd g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g)
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
using hyp3
[PROOF STATE]
proof (prove)
using this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (snd f) = fst (snd g)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have snd_snd: "snd (snd f) = snd (snd g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd f) = snd (snd g)
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
using hyp2
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k)

goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd (snd f) = snd (snd g)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
have fst_det: "fst f = det (fst g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst f = det (fst g)
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
using hyp1
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k))

goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
using this:
fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))

goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst f = det (fst g)

goal (3 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 3. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) \<Longrightarrow>
        fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (let foldl = foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)] in (fst foldl, snd (snd foldl))) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]) = det (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding list_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k]) = det (fst (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k]))
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k)))
[PROOF STEP]
unfolding f_def[symmetric] g_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P f (Suc k)) = det (fst (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst f_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst g_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd f) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
unfolding fst_snd snd_snd fst_det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd g) = fst (snd g) \<Longrightarrow> fst (Gauss_Jordan_column_k_det_P (det (fst g), fst (snd g), snd (snd g)) (Suc k)) = det (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
by (rule det_fst_Gauss_Jordan_column_k_PA_eq_fst_Gauss_Jordan_column_k_det_P)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k])) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) = det (fst (Gauss_Jordan_upt_k_PA A (Suc k)))

goal (2 subgoals):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
 2. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let foldl = foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)] in (fst foldl, snd (snd foldl))) = snd (Gauss_Jordan_upt_k_PA A (Suc k))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]))) = snd (fst (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]), snd (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)])))
[PROOF STEP]
unfolding list_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k]), snd (snd (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k]))) = snd (fst (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k]), snd (snd (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k])))
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k)), snd (snd (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k))))
[PROOF STEP]
unfolding f_def[symmetric] g_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P f (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA g (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
apply (subst f_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA g (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
apply (subst g_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
unfolding fst_snd snd_snd fst_det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (Gauss_Jordan_column_k_det_P (det (fst g), fst (snd g), snd (snd g)) (Suc k)), snd (snd (Gauss_Jordan_column_k_det_P f (Suc k)))) = snd (fst (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)), snd (snd (Gauss_Jordan_column_k_PA g (Suc k))))
[PROOF STEP]
by (metis fst_snd prod.collapse snd_Gauss_Jordan_column_k_det_P_is_snd_Gauss_Jordan_column_k_PA snd_eqD snd_snd)
[PROOF STATE]
proof (state)
this:
snd (Gauss_Jordan_upt_k_det_P A (Suc k)) = snd (Gauss_Jordan_upt_k_PA A (Suc k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>fst (Gauss_Jordan_upt_k_det_P A k) = det (fst (Gauss_Jordan_upt_k_PA A k)); snd (Gauss_Jordan_upt_k_det_P A k) = snd (Gauss_Jordan_upt_k_PA A k); fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]))\<rbrakk> \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
show "fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))
[PROOF STEP]
unfolding list_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) [Suc k])) = fst (snd (foldl Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) [Suc k]))
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc k]) (Suc k)))
[PROOF STEP]
unfolding f_def[symmetric] g_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P f (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst f_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA g (Suc k)))
[PROOF STEP]
apply (subst g_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (fst f, fst (snd f), snd (snd f)) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
unfolding fst_snd snd_snd fst_det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (det (fst g), fst (snd g), snd (snd g)) (Suc k))) = fst (snd (Gauss_Jordan_column_k_PA (fst g, fst (snd g), snd (snd g)) (Suc k)))
[PROOF STEP]
by (rule fst_snd_Gauss_Jordan_column_k_det_P_eq_fst_snd_Gauss_Jordan_column_k_PA)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)])) = fst (snd (foldl Gauss_Jordan_column_k_PA (mat (1::'a), 0, A) [0..<Suc (Suc k)]))

goal:
No subgoals!
[PROOF STEP]
qed