proposition: Lemma mulsmx_subP m1 m2 m n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R : 'A_(m, n)) : reflect (forall A1 A2, A1 \in R1 -> A2 \in R2 -> A1 *m A2 \in R) (R1 * R2 <= R)%MS.
proof: Proof. apply: (iffP memmx_subP) => [sR12R A1 A2 R_A1 R_A2 | sR12R A]. by rewrite sR12R ?mem_mulsmx. case/memmx_sumsP=> A_ -> R_A; rewrite linear_sum summx_sub //= => j _. rewrite (submx_trans (R_A _)) // genmxE; apply/row_subP=> i. by rewrite row_mul mul_rV_lin sR12R ?vec_mxK ?row_sub. 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)