proposition: Lemma plength1_pcore_quo_Sylow G (Gb := G / 'O_p^'(G)) : p.-length_1 G = p.-Sylow(Gb) 'O_p(Gb).
proof: Proof. rewrite /plength_1 eqEsubset pseries_sub /=. rewrite (pseries_rcons _ [:: _; _]) -sub_quotient_pre ?gFnorm //=. rewrite /pHall pcore_sub pcore_pgroup /= -card_quotient ?gFnorm //=. rewrite -quotient_pseries2 /= {}/Gb -(pseries1 _ G). rewrite (card_isog (third_isog _ _ _)) ?pseries_normal ?pseries_sub_catl //. apply/idP/idP=> p'Gbb; last by rewrite (pcore_pgroup_id p'Gbb). exact: pgroupS p'Gbb (pcore_pgroup _ _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)