proposition: Lemma trmx_col : forall m n j0 (A : 'M_(m, n)), (mx_col j0 A)^T === mx_row j0 A^T.
proof: Proof. by rewrite/trmx/mx_row/mx_col=> m n i0 A i j; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms