proposition: Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : (R1 * (R2 * R3) = R1 * R2 * R3)%MS.
proof: Proof. rewrite -(genmx_muls (_ * _)%MS) -genmx_muls; apply/genmxP/andP; split. apply/mulsmx_subP=> A1 A23 R_A1; case/mulsmxP=> A2 R_A2 [A3 R_A3 ->{A23}]. by rewrite !linear_sum summx_sub //= => i _; rewrite mulmxA !mem_mulsmx. apply/mulsmx_subP=> _ A3 /mulsmxP[A1 R_A1 [A2 R_A2 ->]] R_A3. rewrite mulmx_suml linear_sum summx_sub //= => i _. by rewrite -mulmxA !mem_mulsmx. 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)