proposition: Lemma mxsemisimple_reducible V : mxsemisimple V -> mx_completely_reducible V.
proof: Proof. case=> [I W /= simW defV _] U modU sUV; rewrite -defV in sUV. have [J [defV' dxV]] := sum_mxsimple_direct_compl simW modU sUV. exists (\sum_(i in J) W i)%MS. - by apply: sumsmx_module => i _; case: (simW i). - exact: eqmx_trans defV' defV. by rewrite mxdirect_addsE (sameP eqP mxdirect_addsP) /= in dxV; case/and3P: dxV. 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)