proposition: Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) : reflect (exists D, [/\ D.1 \in R1, D.2 \in R2 & A = D.1 + D.2]) (A \in R1 + R2)%MS.
proof: Proof. apply: (iffP sub_addsmxP) => [[u /(canRL mxvecK)->] | [D []]]. exists (vec_mx (u.1 *m R1), vec_mx (u.2 *m R2)). by rewrite /= linearD !vec_mxK !submxMl. case/submxP=> u1 defD1 /submxP[u2 defD2] ->. by exists (u1, u2); rewrite linearD /= defD1 defD2. 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)