[STATEMENT]
lemma matrix_inv_Gauss_Jordan_iarrays_PA:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes inv_A: "invertible A"
shows "matrix_to_iarray (matrix_inv A) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (matrix_inv A) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))
[PROOF STEP]
by (metis inv_A matrix_inv_Gauss_Jordan_PA matrix_to_iarray_fst_Gauss_Jordan_PA)