[STATEMENT]
lemma mat_t_mult_mm [simp]:
  shows "mat_transpose (A *\<^sub>m\<^sub>m B) = mat_transpose B *\<^sub>m\<^sub>m mat_transpose A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_transpose (A *\<^sub>m\<^sub>m B) = mat_transpose B *\<^sub>m\<^sub>m mat_transpose A
[PROOF STEP]
by (cases A, cases B) auto