proposition: Lemma muls0mx m1 m2 n (R2 : 'A_(m2, n)) : ((0 : 'A_(m1, n)) * R2 = 0)%MS.
proof: Proof. apply/eqP; rewrite -submx0; apply/mulsmx_subP=> A0 A2. by rewrite [A0 \in 0]eqmx0 => /memmx0->; rewrite mul0mx mem0mx. 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)