proposition: Proposition beta_not_narrow p : p \in \beta(G) -> [disjoint 'E_p^2(G) & 'E*_p(G)] /\ (forall P, p.-Sylow(G) P -> [disjoint 'E_p^2(P) & 'E*_p(P)]).
proof: Proof. move/forall_inP=> nnG. have nnSyl P: p.-Sylow(G) P -> [disjoint 'E_p^2(P) & 'E*_p(P)]. by move/nnG; rewrite negb_imply negbK setI_eq0 => /andP[]. split=> //; apply/pred0Pn=> [[E /andP[/= Ep2E EpmE]]]. have [_ abelE dimE]:= pnElemP Ep2E; have pE := abelem_pgroup abelE. have [P sylP sEP] := Sylow_superset (subsetT E) pE. case/pred0Pn: (nnSyl P sylP); exists E; rewrite /= 2!inE sEP abelE dimE /=. by rewrite (subsetP (pmaxElemS p (subsetT P))) // inE EpmE inE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)