proposition: Lemma p_elt_gen_length1 G : p.-length_1 G = p^'.-Hall(p_elt_gen p G) 'O_p^'(p_elt_gen p G).
proof: Proof. rewrite /pHall pcore_sub pcore_pgroup pnatNK /= /plength_1. have nUG := p_elt_gen_normal G; have [sUG nnUG]:= andP nUG. apply/idP/idP=> [p1G | pU]. apply: (@pnat_dvd _ #|p_elt_gen p G : 'O_p^'(G)|). by rewrite -[#|_ : 'O_p^'(G)|]indexgI indexgS ?pcoreS. apply: (@pnat_dvd _ #|'O_p(G / 'O_{p^'}(G))|); last exact: pcore_pgroup. rewrite -card_quotient; last first. by rewrite (subset_trans sUG) // normal_norm ?pcore_normal. rewrite -quotient_pseries pseries1 cardSg ?morphimS //=. rewrite gen_subG; apply/subsetP=> x; rewrite inE; case/andP=> Gx p_x. have nOx: x \in 'N('O_{p^',p}(G)). by apply: subsetP Gx; rewrite normal_norm ?pseries_normal. rewrite coset_idr //; apply/eqP; rewrite -[coset _ x]expg1 -order_dvdn. rewrite [#[_]](@pnat_1 p) //; first exact: morph_p_elt. apply: mem_p_elt (pcore_pgroup _ (G / _)) _. by rewrite /= -quotient_pseries /= (eqP p1G); apply/morphimP; exists x. have nOG: 'O_{p^', p}(G) <| G by apply: pseries_normal. rewrite eqEsubset pseries_sub. rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _; _]) //=. rewrite (quotient_pseries [::_; _]) pcore_max //. rewrite /pgroup card_quotient ?normal_norm //. apply: pnat_dvd (indexgS G (_ : p_elt_gen p G \subset _)) _; last first. case p_pr: (prime p); last by rewrite p'natEpi // mem_primes p_pr. rewrite -card_quotient // p'natE //; apply/negP=> /Cauchy[] // Ux. case/morphimP=> x Nx Gx -> /= oUx_p; have:= prime_gt1 p_pr. rewrite -(part_pnat_id (pnat_id p_pr)) -{1}oUx_p {oUx_p} -order_constt. rewrite -morph_constt //= coset_id ?order1 //. by rewrite mem_gen // inE groupX // p_elt_constt. have nOU: p_elt_gen p G \subset 'N('O_{p^'}(G)). by rewrite (subset_trans sUG) // normal_norm ?pseries_normal. rewrite -(quotientSGK nOU) ?(pseries_sub_catl [:: _]) //=. rewrite (quotient_pseries [::_]) pcore_max ?morphim_normal //. rewrite /pgroup card_quotient //= pseries1; apply: pnat_dvd pU. by apply: indexgS; rewrite pcore_max ?pcore_pgroup // gFnormal_trans. 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)