[STATEMENT]
lemma iarray_to_matrix_matrix_to_iarray:
  fixes A::"'a^'columns::{mod_type}^'rows::{mod_type}"
  shows "iarray_to_matrix (matrix_to_iarray A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iarray_to_matrix (matrix_to_iarray A) = A
[PROOF STEP]
unfolding matrix_to_iarray_def iarray_to_matrix_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. IArray (map (\<lambda>x. vec_to_iarray (A $ mod_type_class.from_nat x)) [0..<CARD('rows)]) !! mod_type_class.to_nat i !! mod_type_class.to_nat j) = A
[PROOF STEP]
by (vector, auto, metis IArray.sub_def vec_to_iarray_nth')