proposition: Lemma mx_reducibleS U V : mxmodule U -> (U <= V)%MS -> mx_completely_reducible V -> mx_completely_reducible U.
proof: Proof. move=> modU sUV redV U1 modU1 sU1U. have [W modW defV dxU1W] := redV U1 modU1 (submx_trans sU1U sUV). exists (W :&: U)%MS; first exact: capmx_module. by apply/eqmxP; rewrite !matrix_modl // capmxSr sub_capmx defV sUV /=. by apply/mxdirect_addsP; rewrite capmxA (mxdirect_addsP dxU1W) cap0mx. 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)