proposition: Lemma FTtypeP_facts : [/\ [/\ pred2 2 3 (FTtype S), q < p -> FTtype S == 2, [Frobenius U <*> W1 = U ><| W1] & abelian U], p.-abelem P /\ #|P| = p ^ q, u <= (p ^ q).-1 %/ p.-1, coherent calS S^# tau & normedTI 'A0(S) G S /\ {in 'CF(S, 'A0(S)), tau =1 'Ind}]%N.
proof: Proof. have type23: pred2 2%N 3%N (FTtype S). by rewrite /= -implyNb; apply/implyP=> /type34facts[_ _ [->]]. have [_ ntU _ tiFS] := compl_of_typeII_IV maxS StypeP notStype5. have [_ /mulG_sub[_ sUPU] nPU tiPU] := sdprodP defPU. have cUU: abelian U by case/orP: type23 => [/compl2facts | /compl3facts] [_ ->]. split. - split=> //; last exact: Ptype_compl_Frobenius StypeP _. by rewrite ltnNge; apply: contraR => /type34facts[_ /ltnW]. - by have [/type2facts[] | /type34ker1[]] := boolP (FTtype S == 2%N). - have ->: u = #|U / C|%g by rewrite card_quotient ?normsI ?normG ?norms_cent. have p1gt0: (0 < p.-1)%N by rewrite -(subnKC pgt2). have [/typeP_Galois_P[]| /typeP_Galois_Pn[]]// := boolP (typeP_Galois StypeP). move=> _ _ [_ _]; rewrite pHbar_p CHbar_C // -/u -/q; apply: dvdn_leq. by rewrite divn_gt0 // -!subn1 leq_sub2r // (leq_exp2l 1) ltnW // ltnW. rewrite -/q CHbar_C pHbar_p => H1 [_ _ _ _ [agt1 a_dv_p1 _ [V /card_isog->]]]. apply: leq_trans (_ : p.-1 ^ q.-1 <= _)%N; last first. have ltp1q: (p.-1 ^ q < p ^ q)%N by rewrite ltn_exp2r ?prednK // 2?ltnW. by rewrite leq_divRL // -expnSr (ltn_predK qgt2) -ltnS (ltn_predK ltp1q). rewrite dvdn_leq ?expn_gt0 ?p1gt0 // (dvdn_trans (cardSg (subsetT V))) //. by rewrite cardsT card_mx mul1n dvdn_exp2r //= card_ord Zp_cast. - have:= Ptype_core_coherence maxS StypeP notStype5; rewrite H0_1 CHbar_C. by rewrite (derG1P (abelianS _ cUU)) ?subsetIl ?(group_inj (joing1G _)). have ntA0: 'A0(S) != set0 := FTsupp0_neq0 maxS. suffices tiA0: normedTI 'A0(S) G S by split=> //; apply: Dade_Ind. apply/normedTI_memJ_P=> //; rewrite subsetT; split=> // x g A0x Gg. apply/idP/idP=> [A0xg | /(subsetP (FTsupp0_norm S))/memJ_norm->//]. apply/idPn=> S'g; have Dx: x \in [set y in 'A0(S) | ~~ ('C[y] \subset S)]. rewrite inE A0x; have [_ _ [_ _ _ wccA0 _] _] := pddS. have /imsetP[y Sy Dxy]: x ^ g \in x ^: S by rewrite wccA0 // mem_orbit. apply/subsetPn; exists (g * y^-1)%g; last by rewrite groupMr ?groupV. by rewrite !inE conjg_set1 conjgM Dxy conjgK. have [_ [_ /(_ x Dx) defL] /(_ x Dx)[_ _]] := FTsupport_facts maxS. have{defL} [maxL _] := mem_uniq_mmax defL; set L := 'N[x] in maxL *. rewrite -mem_iota !inE => ALx [/orP[Ltype1 _ | Ltype2]]; last first. by case/(_ _)/existsP=> // ? /Frobenius_of_typeF/(typePF_exclusion StypeP). have /Frobenius_kerP[_ _ _ regLF_L] := FTtype1_Frobenius maxL Ltype1. case/andP: ALx => A1'x /bigcupP[z A1z /setD1P[ntx cLz_z]]; case/negP: A1'x. rewrite ntx /'A1(L) -(Fcore_eq_FTcore _ _) ?(eqP Ltype1) //= in cLz_z A1z *. exact: subsetP (regLF_L z A1z) _ cLz_z. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12)