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