proposition: Lemma mx_trace_block : forall n1 n2 Aul Aur All Alr, \tr (block_mx Aul Aur All Alr : 'M_(n1 + n2)) === \tr Aul + \tr Alr.
proof: Proof. move=> n1 n2 Aul Aur All Alr; rewrite /mx_trace; setoid_rewrite big_split_ord => /=. apply radd_morph; apply eq_bigr=> i _; [rewrite -> block_mxEul | rewrite -> block_mxElr]; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms