proposition: Lemma der_compl_cent_beta' M E : M \in 'M -> \sigma(M)^'.-Hall(M) E -> exists2 H : {group gT}, \beta(M)^'.-Hall(M`_\sigma) H & E^`(1) \subset 'C(H).
proof: Proof. move=> maxM hallE; have [sEM s'E _] := and3P hallE. have s'E': \sigma(M)^'.-group E^`(1) := pgroupS (der_sub 1 E) s'E. have b'E': \beta(M)^'.-group E^`(1). by apply: sub_pgroup s'E' => p; apply: contra; apply: beta_sub_sigma. have solM': solvable M^`(1) := solvableS (der_sub 1 M) (mmax_sol maxM). have [K hallK sE'K] := Hall_superset solM' (dergS 1 sEM) b'E'. exists (K :&: M`_\sigma)%G. apply: Hall_setI_normal hallK. exact: normalS (Msigma_der1 maxM) (der_sub 1 M) (pcore_normal _ M). have nilK: nilpotent K. by have [sKM' b'K _] := and3P hallK; apply: beta'_der1_nil sKM'. rewrite (sub_nilpotent_cent2 nilK) ?subsetIl ?(coprimeSg (subsetIr _ _)) //. exact: pnat_coprime (pcore_pgroup _ _) s'E'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)