proposition: Lemma rsim_regular_series U (compU : mx_composition_series aG U) : (last 0 U :=: 1%:M)%MS -> exists i : 'I_(size U), mx_rsim rG (series_repr i compU).
proof: Proof. move=> lastU; have [V [modV simGV]] := rsim_regular_factmod. have irrV := mx_rsim_irr simGV irrG. have [i simVU] := mx_JordanHolder_max compU lastU irrV. by exists i; apply: mx_rsim_trans simGV simVU. 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)