proposition: Lemma mx_reducible_semisimple V : mxmodule V -> mx_completely_reducible V -> classically (mxsemisimple V).
proof: Proof. move=> modV redV [] // nssimV; have [r leVr] := ubnP (\rank V). elim: r => // r IHr in V leVr modV redV nssimV. have [V0 | nzV] := eqVneq V 0. by rewrite nssimV ?V0 //; apply: mxsemisimple0. apply: (mxsimple_exists modV nzV) => [[U simU sUV]]; have [modU nzU _] := simU. have [W modW defUW dxUW] := redV U modU sUV. have sWV: (W <= V)%MS by rewrite -defUW addsmxSr. apply: IHr (mx_reducibleS modW sWV redV) _ => // [|ssimW]. rewrite ltnS -defUW (mxdirectP dxUW) /= in leVr; apply: leq_trans leVr. by rewrite -add1n leq_add2r lt0n mxrank_eq0. apply: nssimV (eqmx_semisimple defUW (addsmx_semisimple _ ssimW)). exact: mxsimple_semisimple. 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)