proposition: Lemma mx_JordanHolder_exists U V : mx_composition_series U -> modG V -> max_submod V (last 0 U) -> {W : seq 'M_n | mx_composition_series W & last 0 W = V}.
proof: Proof. elim/last_ind: U V => [|U Um IHU] V compU modV; first by case; rewrite ltmx0. rewrite last_rcons => maxV; case/mx_series_rcons: compU => compU modUm maxUm. case eqUV: (last 0 U == V)%MS. case/lastP: U eqUV compU {maxUm IHU} => [|U' Um']. by rewrite andbC; move/eqmx0P->; exists [::]. rewrite last_rcons; move/eqmxP=> eqU'V; case/mx_series_rcons=> compU _ maxUm'. exists (rcons U' V); last by rewrite last_rcons. by apply/mx_series_rcons; split => //; apply: max_submod_eqmx maxUm'. set Um' := last 0 U in maxUm eqUV; have [modU _] := compU. have modUm': modG Um' by rewrite /Um' (last_nth 0) mx_subseries_module'. have [|||W compW lastW] := IHU (V :&: Um')%MS; rewrite ?capmx_module //. by case: (mx_butterfly modUm' modV modUm); rewrite ?eqUV // {1}capmxC. exists (rcons W V); last by rewrite last_rcons. apply/mx_series_rcons; split; rewrite // lastW. by case: (mx_butterfly modV modUm' modUm); rewrite // andbC eqUV. 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)