proposition: Lemma mem_mulsmx m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) A1 A2 : (A1 \in R1 -> A2 \in R2 -> A1 *m A2 \in R1 * R2)%MS.
proof: Proof. move=> R_A1 R_A2; rewrite -[A2]mxvecK; case/submxP: R_A2 => a ->{A2}. rewrite mulmx_sum_row !linear_sum summx_sub // => i _. rewrite !linearZ scalemx_sub {a}//= (sumsmx_sup i) // genmxE. rewrite -[A1]mxvecK; case/submxP: R_A1 => a ->{A1}. by apply/submxP; exists a; rewrite mulmxA mul_rV_lin. 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)