proposition: Theorem BGsummaryI : [/\ forall H x a, Hall G H -> nilpotent H -> x \in H -> x ^ a \in H -> exists2 y, y \in 'N(H) & x ^ a = x ^ y & {in 'M, forall M, FTtype M == 1%N} \/ exists ST : {group gT} * {group gT}, let (S, T) := ST in [/\ S \in 'M /\ T \in 'M, exists Wi : {group gT} * {group gT}, let (W1, W2) := Wi in let W := W1 <*> W2 in let V := W :\: (W1 :|: W2) in [/\ cyclic W, normedTI V G W & W1 :!=: 1 /\ W2 :!=: 1] /\ [/\ S^`(1) ><| W1 = S, T^`(1) ><| W2 = T & S :&: T = W], {in 'M, forall M, FTtype M != 1%N -> exists x, S :^ x = M \/ T :^ x = M}, FTtype S == 2 \/ FTtype T == 2 & 1 < FTtype S <= 5 /\ 1 < FTtype T <= 5]].
proof: Proof. split=> [H x a hallH nilH Hx|]. have [M maxM sHMs] := nilpotent_Hall_sigma nilH hallH. have{} hallH := pHall_subl sHMs (subsetT _) (Hall_pi hallH). by case/(sigma_Hall_tame maxM hallH Hx) => // y; case/setIP; exists y. have [allFM | ] := boolP (('M : {set {group gT}}) \subset 'M_'F). by left=> M maxM; rewrite -FTtype_Fmax // (subsetP allFM). case/subsetPn=> S maxS notFmaxS; right. have PmaxS: S \in 'M_'P by apply/setDP. have [[U W1] /= complU] := kappa_witness maxS; have [_ hallW1 _] := complU. have ntW1: W1 :!=: 1 by rewrite (trivg_kappa maxS). have [[_ [_]]] := BGsummaryC maxS complU ntW1; set W2 := 'C_(_)(W1) => ntW2 _. set W := W1 <*> W2; set V := W :\: _ => _ _ [T [[PmaxT defW1 hallW2 _] _]]. case=> defST _ cycW [P2maxST PmaxST] [tiV _ _] _. have [maxT _] := setDP PmaxT. have [_ _ [_ _ _ _ [_ _ _ defS]]] := Ptype_embedding PmaxS hallW1. have [_ _ [_ _ _ _ [_ _ _ defT]]] := Ptype_embedding PmaxT hallW2. exists (S, T); split=> //; first by exists (W1, [group of W2]). - move=> M maxM; rewrite /= -FTtype_Pmax //. by case/PmaxST/setUP => /imsetP[x _ ->]; exists x; by [left | right]. - by rewrite -!{1}FTtype_P2max. rewrite !{1}(ltn_neqAle 1) -!{1}andbA !{1}FTtype_range // !{1}andbT. by rewrite !{1}(eq_sym 1%N) -!{1}FTtype_Pmax. 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 frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14 BGsection15)