proposition: Lemma trmx_add : forall m n (A B : 'M_(m, n)), (A +m B)^T === A^T +m B^T.
proof: Proof. by move=> m n; rewrite/trmx/null_mx/addmx/oppmx/scalemx; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms