proposition: Lemma pmaxElem_LdivP p G E : prime p -> reflect ('Ldiv_p('C_G(E)) = E) (E \in 'E*_p(G)).
proof: Proof. move=> p_pr; apply: (iffP (pmaxElemP p G E)) => [[] | defE]. case/pElemP=> sEG abelE maxE; have [_ cEE eE] := and3P abelE. apply/setP=> x; rewrite !inE -andbA; apply/and3P/idP=> [[Gx cEx xp] | Ex]. rewrite -(maxE (<[x]> <*> E)%G) ?joing_subr //. by rewrite -cycle_subG joing_subl. rewrite inE join_subG cycle_subG Gx sEG /=. rewrite (cprod_abelem _ (cprodEY _)); last by rewrite centsC cycle_subG. by rewrite cycle_abelem ?p_pr ?orbT // order_dvdn xp. by rewrite (subsetP sEG) // (subsetP cEE) // (exponentP eE). split=> [|H]; last first. case/pElemP=> sHG /abelemP[// | cHH Hp1] sEH. apply/eqP; rewrite eqEsubset sEH andbC /= -defE; apply/subsetP=> x Hx. by rewrite 3!inE (subsetP sHG) // Hp1 ?(subsetP (centsS _ cHH)) /=. apply/pElemP; split; first by rewrite -defE -setIA subsetIl. apply/abelemP=> //; rewrite /abelian -{1 3}defE setIAC subsetIr. by split=> //; apply/exponentP; rewrite -sub_LdivT setIAC subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)