proposition: Lemma addsmxC m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A + B = B + A)%MS.
proof: Proof. have: (A + B == B + A)%MS. by apply/andP; rewrite !addsmx_sub andbC -addsmx_sub andbC -addsmx_sub. move/genmxP; rewrite [@addsmx]unlock -!submx0 !submx0. by do 2!case: eqP => [// -> | _]; rewrite ?genmx_id ?addsmx_nop0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)