proposition: Lemma coprime_typeP_Galois_core g : typeP_Galois StypeP -> g \notin ccG W^# -> g \notin ccG P^# -> coprime #[g] p.
proof: Proof. move=> galS W'g; apply: contraR => p_g. have ntg: g != 1%g by apply: contraNneq p_g => ->; rewrite order1 coprime1n. have [pr_q pr_p]: prime q /\ prime p := FTtypeP_primes maxS StypeP. have [[_ hallW1 _ defS] [_ _ _ defPU] _ [_ _ sW2P _ regPUW1] _] := StypeP. have coPUq: coprime #|PU| q by rewrite (coprime_sdprod_Hall_r defS). have [[_ _ nPUW1 _] [_ _ nPU _]] := (sdprodP defS, sdprodP defPU). have ntP: P :!=: 1%g := mmax_Fcore_neq1 maxS. have frobPU: [Frobenius PU = P ><| U]. have notS5 := FTtype5_exclusion maxS. have inN1 x: x \in 'N(1) by rewrite norm1 inE. have [_ ntU _ _] := compl_of_typeII_IV maxS StypeP notS5. have [] := typeP_Galois_P maxS notS5 galS; rewrite Ptype_factor_prime //. rewrite (group_inj (Ptype_Fcore_kernel_trivial _ _)) // => F [fP [fU _]]. rewrite Ptype_Fcompl_kernel_trivial //. case=> /trivgP injfU fJ [_ /isomP[injfP _] _] _. apply/Frobenius_semiregularP=> // y /setD1P[nty Uy]. apply/trivgP/subsetP=> x /setIP[Px /cent1P-cxy]; apply: contraR nty. rewrite -(morph_injm_eq1 injfU) // -val_eqE -(cosetpre1 1) !(inN1, inE) /=. rewrite -(morph_injm_eq1 injfP) ?mem_quotient //= => /mulfI/inj_eq <-. rewrite mulr1 -[_ * _]fJ ?mem_quotient //= qactE ?dom_qactJ //=. by rewrite conjgE cxy mulKg. have pP: p.-group P by have [_ [/andP[]]] := FTtypeP_facts _ StypeP. have{p_g}[y [a P1a cagy]]: exists y, exists2 a, a \in P^# & g ^ y \in 'C[a]. have sylP: p.-Sylow(G) P. have [/Hall_pi/= hallP _ _] := FTcore_facts maxS; apply: etrans hallP. have [_ _ [n ->]] := pgroup_pdiv pP (mmax_Fcore_neq1 maxS). by apply/eq_pHall => r1; rewrite pi_of_exp ?pi_of_prime. have [y _ Pa] := Sylow_Jsub sylP (subsetT _) (p_elt_constt p g). pose a := g.`_p ^ y; have{} Pa: a \in P by rewrite -cycle_subG cycleJ. exists y, a; last by rewrite cent1C /a conjXg groupX ?cent1id. rewrite !inE conjg_eq1 (contraNneq _ p_g) // => /constt1P/p'nat_coprime-> //. exact: pnat_id. have /(mem_sdprod defS)[x [w [PUx W1w Dgy _]]]: g ^ y \in S. have A0a: a \in 'A0(S) := subsetP (Fcore_sub_FTsupp0 maxS) a P1a. have [_ _ _ _ [tiA0 _]] := FTtypeP_facts _ StypeP. by rewrite (subsetP (cent1_normedTI tiA0 A0a)) // 2!inE. suffices w_eq1: w = 1%g. have sCaP: 'C_PU[a] \subset P := Frobenius_cent1_ker frobPU P1a. rewrite -[g](conjgK y) imset2_f ?inE //= conjg_eq1 ntg /=. by rewrite (subsetP sCaP) // inE cagy Dgy w_eq1 mulg1 PUx. apply: contraNeq W'g => ntw; have nPUw := subsetP nPUW1 w W1w. have{x PUx Dgy} /imset2P[x z W2w_x _ Dgy]: g ^ y \in class_support (W2 :* w) PU. rewrite -(regPUW1 w) ?inE ?ntw // class_supportEr -cover_imset. have coPUw := coprime_dvdr (order_dvdG W1w) coPUq. have [/cover_partition-> _] := partition_cent_rcoset nPUw coPUw. by rewrite Dgy mem_rcoset mulgK. rewrite -[g](conjgK (y * z^-1)%g) imset2_f ?inE //= conjg_eq1 ntg /= conjgM. by rewrite Dgy conjgK -(dprodWC defW) -[x](mulgKV w) mem_mulg -?mem_rcoset. 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 BGappendixC) 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 PFsection13)