proposition: Lemma mx_trace_add : forall n A B, \tr (A +m B : 'M_n) === \tr A + \tr B.
proof: Proof. by move=> n A B; rewrite/mx_trace/addmx; apply big_split. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms