proposition: Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ : reflect (exists2 A_, A = \sum_(i | P i) A_ i & forall i, A_ i \in R_ i) (A \in \sum_(i | P i) R_ i)%MS.
proof: Proof. apply: (iffP sub_sumsmxP) => [[C defA] | [A_ -> R_A] {A}]. exists (fun i => vec_mx (C i *m R_ i)) => [|i]. by rewrite -linear_sum -defA /= mxvecK. by rewrite vec_mxK submxMl. exists (fun i => mxvec (A_ i) *m pinvmx (R_ i)). by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV. 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)