proposition: Lemma mulsmxP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) : reflect (exists2 A1, forall i, A1 i \in R1 & exists2 A2, forall i, A2 i \in R2 & A = \sum_(i < n ^ 2) A1 i *m A2 i) (A \in R1 * R2)%MS.
proof: Proof. apply: (iffP idP) => [R_A|[A1 R_A1 [A2 R_A2 ->{A}]]]; last first. by rewrite linear_sum summx_sub // => i _; rewrite mem_mulsmx. have{R_A}: (A \in R1 * <<R2>>)%MS. by apply: memmx_subP R_A; rewrite mulsmxS ?genmxE. case/memmx_sumsP=> A_ -> R_A; pose A2_ i := vec_mx (row i <<R2>>%MS). pose A1_ i := mxvec (A_ i) *m pinvmx (R1 *m lin_mx (mulmxr (A2_ i))) *m R1. exists (vec_mx \o A1_) => [i|]; first by rewrite vec_mxK submxMl. exists A2_ => [i|]; first by rewrite vec_mxK -(genmxE R2) row_sub. apply: eq_bigr => i _; rewrite -[_ *m _](mx_rV_lin (mulmxr (A2_ i))). by rewrite -mulmxA mulmxKpV ?mxvecK // -(genmxE (_ *m _)) R_A. 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)