proposition: Lemma sum_mxsimple_direct_sub I W (V : 'M_n) : (forall i : I, mxsimple (W i)) -> (\sum_i W i :=: V)%MS -> {J : {set I} | let S := \sum_(i in J) W i in S :=: V /\ mxdirect S}%MS.
proof: Proof. move=> simW defV. have [|J [defS dxS]] := sum_mxsimple_direct_compl simW (mxmodule0 n). exact: sub0mx. exists J; split; last by rewrite mxdirectE /= adds0mx mxrank0 in dxS. by apply: eqmx_trans defV; rewrite adds0mx_id in defS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)