proposition: Lemma sigma'_kappa'_facts M p S (A := 'Ohm_1(S)) (Ms := M`_\sigma) : M \in 'M -> p.-Sylow(M) S -> [&& p \in \pi(M), p \notin \sigma(M) & p \notin \kappa(M)] -> [/\ M \in 'M_'F :|: 'M_'P2, logn p #|A| <= 2, 'C_Ms(A) = 1 & nilpotent Ms].
proof: Proof. move=> maxM sylS /and3P[piMp sM'p kM'p]; have [sSM pS _] := and3P sylS. rewrite 8!(maxM, inE) /= !andbT negb_and orb_andr orbN andbT negbK. rewrite (contra (fun skM => pnatPpi skM piMp)) ?orbT; last exact/norP. rewrite partition_pi_mmax // (negPf sM'p) orbF orbCA in piMp. have{piMp} [t2p | t13p] := orP piMp. rewrite (tau2_Msigma_nil maxM t2p); have [_ rpM] := andP t2p. have{rpM} rS: 2 <= 'r_p(S) by rewrite (p_rank_Sylow sylS) (eqP rpM). have [B EpB] := p_rank_geP rS; have{EpB} [sBS abelB dimB] := pnElemP EpB. have EpB: B \in 'E_p^2(M) by rewrite !inE abelB dimB (subset_trans sBS). have [defB _ regB _ _] := tau2_context maxM t2p EpB. by rewrite /A -dimB; have [_ [|->]] := defB S sylS. have [ntS cycS]: S :!=: 1 /\ cyclic S. rewrite (odd_pgroup_rank1_cyclic pS) ?mFT_odd // (p_rank_Sylow sylS). apply/andP; rewrite -rank_gt0 (rank_Sylow sylS) -eqn_leq eq_sym. by rewrite -2!andb_orr orNb andbT inE /= sM'p in t13p. have [p_pr _ _] := pgroup_pdiv pS ntS. have oA: #|A| = p by rewrite (Ohm1_cyclic_pgroup_prime cycS pS). have sAM: A \subset M by apply: gFsub_trans. have regA: 'C_Ms(A) = 1. apply: contraNeq kM'p => nregA; rewrite unlock; apply/andP; split=> //. by apply/exists_inP; exists [group of A]; rewrite ?p1ElemE // !inE sAM oA /=. have defMsA: Ms ><| A = Ms <*> A. rewrite sdprodEY ?coprime_TIg ?(subset_trans sAM) ?gFnorm // oA. by rewrite (pnat_coprime (pcore_pgroup _ _)) ?pnatE. rewrite (prime_Frobenius_sol_kernel_nil defMsA) ?oA ?(pfactorK 1) //. by rewrite (solvableS _ (mmax_sol maxM)) // join_subG pcore_sub. 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)