proposition: Lemma mx_JordanHolder_max U (m := size U) V compU modV : (last 0 U :=: 1%:M)%MS -> mx_irreducible (@factmod_repr _ G n rG V modV) -> exists i : 'I_m, mx_rsim (factmod_repr modV) (@series_repr U i compU).
proof: Proof. rewrite {}/m; set Um := last 0 U => Um1 irrV. have modUm: modG Um := last_mod compU; have simV := rsimC (mx_factmod_sub modV). have maxV: max_submod V Um. move/max_submodP: (mx_rsim_irr simV irrV) => /(_ (submx1 _)). by apply: max_submod_eqmx; last apply: eqmx_sym. have [W compW lastW] := mx_JordanHolder_exists compU modV maxV. have compWU: mx_series (rcons W Um) by apply/mx_series_rcons; rewrite lastW. have:= mx_JordanHolder compU compWU; rewrite last_rcons size_rcons. case=> // szW [p pUW]; have ltWU: size W < size U by rewrite szW. pose i := Ordinal ltWU; exists ((p^-1)%g i). apply: rsimT simV (rsimT _ (rsimC (pUW _))); rewrite permKV. apply: rsimT (rsimC _) (rsim_last (last_mod compW) modUm _). by apply: section_eqmx; rewrite ?lastW. 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)