proposition: Theorem nonTI_Fitting_structure M g (H := (M`_\F)%G) : let X := ('F(M) :&: 'F(M) :^ g)%G in M \in 'M -> g \notin M -> X :!=: 1 -> [/\ M \in 'M_'F :|: 'M_'P1 /\ H :=: M`_\sigma, X \subset H /\ cyclic X, M^`(1) \subset 'F(M) /\ M`_\sigma \x 'O_\sigma(M)^'('F(M)) = 'F(M), forall E E1 E2 E3, sigma_complement M E E1 E2 E3 -> [/\ E3 :=: 1, E2 <| E, E / E2 \isog E1 & cyclic (E / E2)] & [/\ M \in 'M_'F, abelian H & 'r(H) = 2] \/ let p := #|X| in [/\ prime p, ~~ abelian 'O_p(H), cyclic 'O_p^'(H) & {in \pi(H), forall q, exponent (M / H) %| q.-1} \/ [/\ #|'O_p(H)| = (p ^ 3)%N, M \in 'M_'P1 & #|M / H| %| p.+1] ]].
proof: Proof. move=> X maxM notMg ntX; have nilH: nilpotent H := Fcore_nil M. have /andP[sHM nHM]: H <| M := Fcore_normal M. have [[cycY t2Y] [_ _ defF] _ _] := Fitting_structure maxM. set Y := 'O_\sigma(M)^'('F(M)) in cycY t2Y defF *. have not_cycMp: {in \pi(X), forall p, ~~ cyclic 'O_p(M)}. move=> p; rewrite mem_primes => /and3P[p_pr _ p_dv_X]. apply: contra notMg => cycMp. have hallMp := nilpotent_pcore_Hall p (Fitting_nil M). have{cycMp} defNx1: {in 'F(M), forall x1, #[x1] = p -> 'N(<[x1]>) = M}. move=> x1; rewrite /order -cycle_subG => sX1F oX1. rewrite (mmax_normal maxM) //; last by rewrite -cardG_gt1 oX1 prime_gt1. rewrite (char_normal_trans _ (pcore_normal p M)) ?sub_cyclic_char //=. by rewrite -p_core_Fitting (sub_Hall_pcore hallMp) // /pgroup oX1 pnat_id. have [x1 Xx1 ox1] := Cauchy p_pr p_dv_X; have [Fx1 Fgx1] := setIP Xx1. rewrite -(norm_mmax maxM) inE -{1}(defNx1 (x1 ^ g^-1)) -?mem_conjg ?orderJ //. by rewrite cycleJ normJ actKV -(defNx1 x1). have{cycY} sX: \sigma(M).-group X. apply: sub_pgroup (pgroup_pi X) => p piXp. apply: contraR (not_cycMp p piXp) => s'p; rewrite -p_core_Fitting. by apply: cyclicS (sub_pcore _ _) cycY => p1; move/eqnP->. have sXMs: X \subset M`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) // subIset ?Fitting_sub. have E1X_facts p X1 (C1 := 'C_H(X1)%G): X1 \in 'E_p^1(X) -> [/\ C1 \notin 'U, 'r(C1) <= 2 & abelian C1]. - move=> EpX1; have [sX1X /andP[pX1 _] _] := pnElemP EpX1. have piXp: p \in \pi(X) by rewrite -p_rank_gt0; apply/p_rank_geP; exists X1. have not_sCX1M: ~~ ('C(X1) \subset M). have [[sX1F sX1Fg] sFM] := (subsetIP sX1X, Fitting_sub M). apply: contra notMg => sCX1M; rewrite -groupV. have [trCX1 _ _] := sigma_group_trans maxM (pnatPpi sX piXp) pX1. have [||c cX1c] := trCX1 g^-1; rewrite ?(subset_trans _ sFM) ?sub_conjgV //. by case=> m Mm ->; rewrite groupM // (subsetP sCX1M). have ltCX1_G: 'C(X1) \proper G := mFT_cent_proper (nt_pnElem EpX1 isT). have ltC1G: C1 \proper G := sub_proper_trans (subsetIr H _) ltCX1_G. have{ltCX1_G} nonuniqC1: C1 \notin 'U. have sC1M: C1 \subset M by rewrite subIset ?Fcore_sub. apply: contra not_sCX1M => uniqC1. by rewrite (sub_uniq_mmax (def_uniq_mmax uniqC1 maxM sC1M)) ?subsetIr. split=> //; first by rewrite leqNgt (contra (rank3_Uniqueness _)). have sC1H: C1 \subset H := subsetIl _ _. have dprodC1: 'F(C1) = C1 := nilpotent_Fitting (nilpotentS sC1H nilH). apply/center_idP; rewrite -{2}dprodC1 -(center_bigdprod dprodC1). apply: eq_bigr => r _; apply/center_idP; apply: contraR nonuniqC1. move/(nonabelian_Uniqueness (pcore_pgroup _ _)). exact: uniq_mmaxS (pcore_sub _ _) ltC1G. pose p := pdiv #|X|; have piXp: p \in \pi(X) by rewrite pi_pdiv cardG_gt1. have /p_rank_geP[X1 EpX1]: 0 < 'r_p(X) by rewrite p_rank_gt0. have [sMp ntX1] := (pnatPpi sX piXp, nt_pnElem EpX1 isT). have [p_pr oX1] := (pnElem_prime EpX1, card_pnElem EpX1 : #|X1| = p). have [sX1X abelX1 dimX1] := pnElemP EpX1; have [pX1 _] := andP abelX1. have [nonuniqC1 rC1 cC1C1] := E1X_facts p X1 EpX1. have [cycX b'p]: cyclic X /\ p \in \beta(M)^'. have [E hallE] := ex_sigma_compl maxM. have [_ _] := sigma_compl_embedding maxM hallE. case/(_ g notMg); set X2 := _ :&: _ => cycX2 b'X2 _. have sXMg: X \subset M :^ g by rewrite subIset // conjSg Fitting_sub orbT. have{sXMg} sXX2: X \subset X2 by rewrite subsetI sXMs. by rewrite (pnatPpi b'X2 (piSg sXX2 piXp)) (cyclicS sXX2). have b'H: \beta(M)^'.-group H. apply: sub_pgroup (pgroup_pi _) => r piHr; have [-> // | p'r] := eqVneq r p. apply/existsP; exists 'O_r(M)%G; rewrite /= Fcore_pcore_Sylow // negbK. apply/implyP; rewrite ltnNge -rank_pgroup ?pcore_pgroup ?(leq_trans _ rC1) //. rewrite rankS // subsetI /= -{1}(p_core_Fcore piHr) pcore_sub //. rewrite -p_core_Fitting (sub_nilpotent_cent2 (Fitting_nil M)) ?pcore_sub //. exact: subset_trans sX1X (subsetIl _ _). exact: pnat_coprime pX1 (pi_pgroup (pcore_pgroup r _) _). have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). have [sKM kK _] := and3P hallK; have s'K := sub_pgroup (@kappa_sigma' _ M) kK. have [U complU] := ex_kappa_compl maxM hallK. have [[defM cycK _] defM' _ _ exU0] := kappa_structure maxM complU. have{b'p} FP1maxM: M \in 'M_'F :|: 'M_'P1. apply: contraR b'p; rewrite inE /=; case/norP=> notFmaxF notP1maxF. have PmaxM: M \in 'M_'P by apply/setDP. by have [_ _ _ _ [| <- //]] := Ptype_structure PmaxM hallK; apply/setDP. have defH: H :=: M`_\sigma. apply/eqP; apply/idPn=> neqHMs; pose q := #|'C_(M`_\sigma)(K)|. have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM). have [D hallD] := Hall_exists q^' solMs. have [_ /(_ K D)[] // _ [_ _ piHq /idPn[]]] := Fcore_structure maxM. exact: pnatPpi b'H piHq. have{sXMs} sXH: X \subset H by rewrite defH. have{b'H} sM'F: M^`(1) \subset 'F(M). rewrite Fitting_max ?der_normal // (isog_nil (quotient1_isog _)). suffices <-: M`_\beta = 1 by apply: Mbeta_quo_nil. apply/eqP; rewrite trivg_card1 (card_Hall (Mbeta_Hall maxM)). rewrite -(partn_part _ (beta_sub_sigma maxM)) -(card_Hall (Msigma_Hall maxM)). by rewrite /= -defH partG_eq1. have{} defF: M`_\sigma \x Y = 'F(M). by rewrite -defF -defH nilpotent_Fitting. split=> // [E E1 E2 E3 complEi | {Y t2Y defF sM'F}]. have [[sE3E' _] _ [cycE1 _] [_ defE] _]:= sigma_compl_context maxM complEi. have [hallE _ _ hallE3 _] := complEi; have [sE3E t3E3 _] := and3P hallE3. have E3_1: E3 :=: 1. have [sEM s'E _] := and3P hallE; have sE'M' := dergS 1 sEM. have sE3F: E3 \subset 'F(M) := subset_trans sE3E' (subset_trans sE'M' sM'F). rewrite -(setIidPr sE3F) coprime_TIg // -(dprod_card defF) coprimeMl. rewrite (pnat_coprime (pcore_pgroup _ _) (pgroupS sE3E s'E)). exact: p'nat_coprime (sub_pgroup (@tau3'2 _ M) t2Y) t3E3. have{} defE: E2 ><| E1 = E by rewrite -defE E3_1 sdprod1g. have [-> _ mulE21 nE21 tiE21] := sdprod_context defE. by rewrite -mulE21 quotientMidl quotient_cyclic // isog_sym quotient_isog. have{defM'} defM_P1: M \in 'M_'P1 -> H ><| K = M /\ M^`(1) = H. move=> P1maxM; have [PmaxM _] := setIdP P1maxM. have U1: U :=: 1 by apply/eqP; rewrite (trivg_kappa_compl maxM complU). have ntK: K :!=: 1 by rewrite (trivg_kappa maxM hallK); case/setDP: PmaxM. by have [<- _] := defM' ntK; rewrite -{1}defM U1 sdprodg1 -defH. pose P := 'O_p(H); have sylP: p.-Sylow(H) P := nilpotent_pcore_Hall p nilH. have [sPH pP _] := and3P sylP. have [cHH | {not_cycMp} not_cHH] := boolP (abelian H); [left | right]. have [-> | P1maxM] := setUP FP1maxM; last first. have [PmaxM _] := setIdP P1maxM. have [ntKs _ sKsM'' _ _] := Ptype_cyclics PmaxM hallK. case/eqP: (subG1_contra sKsM'' ntKs); apply/derG1P. by rewrite /= -derg1; have [_ ->] := defM_P1 P1maxM. split=> //; apply/eqP; rewrite eqn_leq (leq_trans _ rC1) //=; last first. by rewrite rankS // subsetIidl (centsS sX1X) // (sub_abelian_cent cHH). apply: leq_trans (rankS (pcore_sub p _)). rewrite ltnNge -abelian_rank1_cyclic ?(abelianS sPH) //=. by rewrite p_core_Fcore ?(piSg sXH) ?not_cycMp. have sX1P: X1 \subset P by rewrite (sub_Hall_pcore sylP) ?(subset_trans sX1X). have [_ mulPHp' cPHp' _] := dprodP (nilpotent_pcoreC p nilH : P \x _ = H). have cHp'Hp': abelian 'O_p^'(H). by rewrite (abelianS _ cC1C1) // subsetI pcore_sub (centsS sX1P). have not_cPP: ~~ abelian P. by apply: contra not_cHH => cPP; rewrite -mulPHp' abelianM cPP cHp'Hp'. have{E1X_facts} pX: p.-group X. apply: sub_pgroup (pgroup_pi _) => q; rewrite -p_rank_gt0. case/p_rank_geP=> X2 EqX2; have [_ _ cC2C2] := E1X_facts _ _ EqX2. case/pnElemP: EqX2 => sX2X /andP[qX2 _] _; have sX2H := subset_trans sX2X sXH. apply: contraR not_cPP => q'p; rewrite (abelianS _ cC2C2) // subsetI sPH. by rewrite (sub_nilpotent_cent2 nilH) ?(p'nat_coprime (pi_pgroup qX2 _) pP). have sXP: X \subset P by rewrite (sub_Hall_pcore sylP). pose Z0 := 'Ohm_1('Z(P)); have sZ0ZP: Z0 \subset 'Z(P) := Ohm_sub 1 _. have{sZ0ZP} [sZ0P cPZ0] := subsetIP sZ0ZP. have not_sX1Z0: ~~ (X1 \subset Z0). apply: contra not_cPP => sX1Z0; apply: abelianS cC1C1. by rewrite subsetI sPH (centsS sX1Z0) // centsC. pose B := X1 <*> Z0; have sBP: B \subset P by rewrite join_subG sX1P. have defB: X1 \x Z0 = B by rewrite dprodEY ?prime_TIg ?oX1 ?(centsS sX1P). have pZP: p.-group 'Z(P) := pgroupS (center_sub _) pP. have abelZ0: p.-abelem Z0 by rewrite Ohm1_abelem ?center_abelian. have{abelZ0} abelB: p.-abelem B by rewrite (dprod_abelem _ defB) abelX1. have sylP_Ms: p.-Sylow(M`_\sigma) P by rewrite -defH. have sylP_G: p.-Sylow(G) P := subHall_Sylow (Msigma_Hall_G maxM) sMp sylP_Ms. have max_rB A: p.-abelem A -> B \subset A -> 'r_p(A) <= 2. move=> abelA /joing_subP[sX1A _]; have [pA cAA _] := and3P abelA. suffices [a [nX1a sAaP]]: exists a, a \in 'N(X1) /\ A :^ a \subset P. rewrite -rank_pgroup // -(rankJ _ a) (leq_trans _ rC1) ?rankS //= subsetI. by rewrite -(normP nX1a) centJ conjSg (subset_trans sAaP) ?(centsS sX1A). have [a _ sAaP] := Sylow_Jsub sylP_G (subsetT A) pA. have [x1 defX1]: exists x1, X1 :=: <[x1]>. by apply/cyclicP; rewrite prime_cyclic ?oX1. have Px1: x1 \in P by rewrite -cycle_subG -defX1. have Px1a: x1 ^ a \in P. by rewrite (subsetP sAaP) // memJ_conjg -cycle_subG -defX1. have [b nPb def_xb] := sigma_Hall_tame maxM sylP_Ms Px1 Px1a. exists (a * b^-1); rewrite !inE !actM !sub_conjgV defX1 /= -!cycleJ def_xb. by have{nPb} [_ nPb] := setIP nPb; rewrite (normP nPb). have rpB: 'r_p(B) = 2. apply/eqP; rewrite eqn_leq max_rB // -(p_rank_dprod p defB). rewrite p_rank_abelem ?dimX1 // ltnS p_rank_Ohm1 -rank_pgroup // rank_gt0. by rewrite center_nil_eq1 ?(pgroup_nil pP) ?(subG1_contra sXP). have oZ0: #|Z0| = p. apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 X1)) (dprod_card defB) oX1. by rewrite (card_pgroup (abelem_pgroup abelB)) -p_rank_abelem ?rpB. have p2maxElemB: [group of B] \in 'E_p^2(G) :&: 'E*_p(G). rewrite !inE subsetT abelB -p_rank_abelem // rpB /=. apply/maxgroupP; rewrite !inE subsetT /= -/B; split=> // A. case/pElemP=> _ abelA sBA; have [pA _] := andP abelA. apply/eqP; rewrite eq_sym eqEcard sBA (card_pgroup pA). rewrite (card_pgroup (abelem_pgroup abelB)) -!p_rank_abelem // rpB. by rewrite leq_exp2l ?prime_gt1 ?max_rB. have{not_sX1Z0} defX: X :=: X1. have sX_CPB: X \subset 'C_P(B). rewrite centY !subsetI sXP sub_abelian_cent ?cyclic_abelian //=. by rewrite centsC (centsS sXP). have [C defCPB]: exists C, X1 \x C = 'C_P(B). have [_ [C]] := basic_p2maxElem_structure p2maxElemB pP sBP not_cPP. case=> _ _ defCPB _; exists C; rewrite defCPB // !inE joing_subl abelX1. by rewrite -val_eqE eqEsubset negb_and not_sX1Z0 /= dimX1. have defX: X1 \x (C :&: X) = X by rewrite (dprod_modl defCPB) // (setIidPr _). by move/eqP: ntX1; case/(cyclic_pgroup_dprod_trivg pX cycX): defX; case. have cycHp': cyclic 'O_p^'(H). rewrite abelian_rank1_cyclic // leqNgt; apply: contra nonuniqC1 => rHp'. apply: (uniq_mmaxS (setIS H (centS sX1P))). by rewrite mFT_sol_proper nilpotent_sol // (nilpotentS (subsetIl _ _)). apply: cent_uniq_Uniqueness (subsetIr _ _) (leq_trans rHp' (rankS _)). exact: nonabelian_Uniqueness pP not_cPP. by rewrite subsetI pcore_sub. rewrite {1}defX oX1 /= -[M`_\F]/(gval H) -/P; split=> //. pose Z q := 'Ohm_1('Z('O_q(H)))%G. have charZ q: Z q \char H by rewrite 3?gFchar_trans. have{cycHp'} oZ: {in \pi(H), forall q, #|Z q| = q}. move=> q piHp; have [-> // | p'q] := eqVneq q p. have qHq: q.-group 'O_q(H) := pcore_pgroup q H. have sHqHp': 'O_q(H) \subset 'O_p^'(H) by apply: sub_pcore => r /eqnP->. rewrite /= (center_idP (abelianS sHqHp' cHp'Hp')). apply: Ohm1_cyclic_pgroup_prime (cyclicS sHqHp' cycHp') qHq _. by rewrite -rank_gt0 (rank_Sylow (nilpotent_pcore_Hall q nilH)) p_rank_gt0. have regZq_dv_q1 A q: A \subset 'N(H) -> q \in \pi(H) -> semiregular (Z q) A -> #|A| %| q.-1. - move=> nHA piHq regA. by rewrite -(oZ q piHq) regular_norm_dvd_pred // (char_norm_trans (charZ q)). have [FmaxM | {U complU defM exU0}P1maxM] := setUP FP1maxM. left=> q piHq; have K1: K :=: 1 by apply/eqP; rewrite (trivg_kappa maxM). have ntU: U :!=: 1 by rewrite (trivg_kappa_compl maxM complU) 2!inE FmaxM. rewrite K1 sdprodg1 -defH in defM; have [_ mulHU nHU tiHU] := sdprodP defM. rewrite -mulHU quotientMidl -(exponent_isog (quotient_isog nHU tiHU)). have [U0 [sU0U <- frobMsU0]] := exU0 ntU; have nHU0 := subset_trans sU0U nHU. apply: dvdn_trans (exponent_dvdn U0) _; apply: regZq_dv_q1 => // x U0x. apply/trivgP; rewrite -(Frobenius_reg_ker frobMsU0 U0x) setSI //= -defH. exact: (char_sub (charZ _)). have{defM_P1} [[defM defM'] [PmaxM _]] := (defM_P1 P1maxM, setIdP P1maxM). have [_ mulHK nHK tiHK] := sdprodP defM; have p'K := pi'_p'group s'K sMp. have coHK: coprime #|H| #|K| by rewrite defH (pnat_coprime (pcore_pgroup _ _)). have{coHK} coPK: coprime #|P| #|K| := coprimeSg sPH coHK. have oMH: #|M / H| = #|K|. by rewrite -mulHK quotientMidl -(card_isog (quotient_isog nHK tiHK)). pose Ks := 'C_H(K); have prKs: prime #|Ks|. have [Ms _ [_ _ _ _ [_]]] := Ptype_embedding PmaxM hallK. by rewrite inE P1maxM -defH; do 2!case. have sKsP: Ks \subset P. have sKsM'': Ks \subset M^`(2) by rewrite /Ks defH; case/Ptype_cyclics: hallK. rewrite (subset_trans sKsM'') 1?der1_min //= -derg1 defM' ?gFnorm //. by rewrite -mulPHp' quotientMidl quotient_abelian. have oKs: #|Ks| = p. apply/eqP; apply: pnatPpi pP (piSg sKsP _). by rewrite mem_primes prKs cardG_gt0 dvdnn. have [prHK ntKs]: semiprime H K /\ Ks != 1. by rewrite /Ks defH; case/Ptype_structure: hallK => // [[_ _ [_ ? _]] _ []]. have [K_dv_p1 | {regZq_dv_q1}] := altP (@implyP (Ks :==: Z0) (#|K| %| p.-1)). left=> q piHq; rewrite (dvdn_trans (exponent_dvdn _)) // oMH. have [eqZqKs | neqZqKs] := eqVneq Ks (Z q). have def_q: q = p by rewrite -(oZ q piHq) -eqZqKs. by rewrite def_q K_dv_p1 // eqZqKs def_q. apply: regZq_dv_q1 => // x Kx; rewrite -(setIidPl (char_sub (charZ q))). rewrite -setIA prHK {x Kx}// setIC (prime_TIg prKs) //. have q_pr: prime q by rewrite mem_primes in piHq; case/and3P: piHq. apply: contra neqZqKs => sKsZq; rewrite eqEsubset sKsZq /=. by rewrite prime_meetG ?oZ // (setIidPr sKsZq). rewrite {Z oZ charZ}negb_imply; case/andP; move/eqP=> defKs not_K_dv_p1. have nPK: K \subset 'N(P) by apply: gFnorm_trans. have defZP: 'Z(P) = Ks. apply/eqP; rewrite eqEsubset andbC {1}defKs Ohm_sub subsetI subIset ?sPH //. have nZPK: K \subset 'N('Z(P)) by apply: gFnorm_trans. have coZPK: coprime #|'Z(P)| #|K| := coprimeSg (center_sub _) coPK. rewrite centsC (coprime_odd_faithful_Ohm1 pZP) ?mFT_odd //. by rewrite /= -/Z0 -defKs centsC subsetIr. have rPle2: 'r(P) <= 2. case/setIP: p2maxElemB; case/pnElemP=> _ _ dimB pmaxB. have Ep2B: [group of B] \in 'E_p^2(P) by apply/pnElemP. rewrite leqNgt; apply: contra not_K_dv_p1 => rPgt2. have tiKcP: 'C_K(P) = 1. apply/trivgP/subsetP=> x => /setIP[Kx cPx]. apply: contraR ntX1 => ntx; rewrite -subG1. have [_ _ _ <-] := dprodP defB; rewrite subsetIidl -defKs. rewrite -[Ks](prHK x) 1?inE ?ntx // (subset_trans sX1P) //=. by rewrite subsetI sPH sub_cent1. rewrite (card_isog (quotient1_isog _)) -tiKcP -ker_conj_aut. rewrite (card_isog (first_isog_loc _ nPK)) /=. set A := _ @* _; have AutA: A \subset Aut P := Aut_conj_aut _ _. have solA: solvable A by rewrite morphim_sol ?abelian_sol ?cyclic_abelian. have oddA: odd #|A| by rewrite morphim_odd ?mFT_odd. have nnP: p.-narrow P. apply/implyP=> _; apply/set0Pn; exists [group of B]. by rewrite inE Ep2B (subsetP (pmaxElemS p (subsetT P))) // inE pmaxB inE. have [x defK] := cyclicP cycK; have Kx: x \in K by rewrite defK cycle_id. have nPx := subsetP nPK x Kx; rewrite /A defK morphim_cycle //. have Axj: conj_aut [group of P] x \in A by apply: mem_morphim. have [_ _ -> //] := Aut_narrow pP (mFT_odd _) nnP solA AutA oddA. by rewrite morph_p_elt // (mem_p_elt p'K). have{rPle2} dimP: logn p #|P| = 3. have [S [_ <- _] [C cycC]] := mFT_rank2_Sylow_cprod sylP_G rPle2 not_cPP. case=> defP defZS; congr (logn p #|(_ : {set _})|). suffices defC: 'Ohm_1(C) = C by rewrite -defC defZS cprod_center_id in defP. suffices <-: 'Z(P) = C by rewrite defZP (@Ohm1_id _ p) // prime_abelem. have [_ <- _] := cprodP (center_cprod defP). by rewrite -defZS (center_idP (cyclic_abelian cycC)) mulSGid ?Ohm_sub. have oP: #|P| = (p ^ 1.*2.+1)%N by rewrite (card_pgroup pP) dimP. right; split; rewrite // {}oMH. have esP: extraspecial P by apply: (p3group_extraspecial pP); rewrite ?dimP. have defPK: P ><| K = P <*> K by rewrite sdprodEY // coprime_TIg. have copK: coprime p #|K| by rewrite -oX1 (coprimeSg sX1P). have [x|] := repr_extraspecial_prime_sdprod_cycle pP esP defPK cycK oP copK. move/prHK=> defCHx /=; rewrite /= -/P -{1}(setIidPl sPH) -setIA defCHx -/Ks. by rewrite -defZP setIA setIid. by rewrite addn1 subn1 (negPf not_K_dv_p1) orbF. 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 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)