proposition: Corollary ell_sigma_leq_2 x : \ell_\sigma(x) <= 2.
proof: Proof. have [/ell_sigma0P/eqP-> // | ntx] := eqVneq x 1. case sigma_x: (x \in cover [set class_support M^~~ G | M : {group gT} in 'M]). case/bigcupP: sigma_x => _ /imsetP[M maxM ->]. case/imset2P=> x0 a /bigcupP[y Ms_y yRx0] _ ->; rewrite ell_sigmaJ. exact: ell_sigma_cover (Msigma_ell1 maxM Ms_y) yRx0. have G1x: x \in G^# by rewrite !inE andbT. have [FpartG1 PpartG1] := mFT_partition. have [/eqP/FpartG1 partG1 | [M PmaxM]] := set_0Vmem ('M_'P : {set {group gT}}). by rewrite -(cover_partition partG1) sigma_x in G1x. have [maxM _] := setDP PmaxM. have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). have{PpartG1} [/cover_partition defG1 notZsigma] := PpartG1 M K PmaxM hallK. rewrite -{}defG1 /cover big_setU1 {notZsigma}// inE {}sigma_x orbF in G1x. case/imset2P: G1x => x0 a /setDP[]. have [Mst [PmaxMst _] [_ _ [defK _] _ _]] := Ptype_embedding PmaxM hallK. rewrite cent_joinEr ?subsetIr // => /mulsgP[y' y Ky' /= Ks_y ->]. rewrite inE; have [-> | nty] := eqVneq y 1; first by rewrite mulg1 Ky'. have [-> | nty' _ _ ->] := eqVneq y' 1; first by rewrite mul1g Ks_y orbT. have [Ms_y cKy] := setIP Ks_y; set Ks := 'C_(_)(_) in Ks_y defK. have Msts_y': y' \in Mst`_\sigma by move: Ky'; rewrite -defK => /setIP[]. have kMy': \kappa(M).-elt y' := mem_p_elt (pHall_pgroup hallK) Ky'. have{kMy'} sM'y': \sigma(M)^'.-elt y' := sub_pgroup (@kappa_sigma' _) kMy'. rewrite ell_sigmaJ /sigma_length (cardsD1 (y' * y).`_\sigma(M)). rewrite (leq_add (leq_b1 _)) // -sigma_decomposition_constt' //. rewrite consttM /commute ?(centP cKy) // constt_p_elt //. rewrite (constt1P _) ?p_eltNK ?(mem_p_elt (pcore_pgroup _ _) Ms_y) // mulg1. have [maxMst _] := setDP PmaxMst; rewrite leq_eqVlt (Msigma_ell1 maxMst) //. by rewrite !inE nty' Msts_y'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)