proposition: Lemma card_FTtypeP_Galois_compl : typeP_Galois StypeP -> u = (if p == 1 %[mod q] then ustar %/ q else ustar).
proof: Proof. case/typeP_Galois_P=> //= _ _ [_ _ /dvdnP[b]]; rewrite Ptype_factor_prime //. rewrite -/ustar Ptype_Fcompl_kernel_trivial -(card_isog (quotient1_isog _)) -/u. move=> Dbu; have ub_b: (b <= q.*2)%N. have [[lambda Slam irrHlam]| ] := altP (@hasP _ irrIndH calS). apply: (FTtypeP_Ind_Fitting_Galois_ub Slam irrHlam). by rewrite FTtypeP_reg_Fcore indexg1. case/(FTtypeP_no_Ind_Fitting_facts maxS StypeP) => _ /= ->. rewrite indexg1 -/ustar -(leq_pmul2r (cardG_gt0 U)) -/u => Du. by rewrite -Dbu -Du -(subnKC qgt2) leq_pmull. have [ustar_odd p1_q p'1_q] := FTtypeP_primes_mod_cases. have b_odd: odd b by rewrite Dbu oddM mFT_odd andbT in ustar_odd. case: ifPn => [/p1_q q_dv_ustar | /p'1_q[_ _ /(_ b)]]. have /dvdnP[c Db]: q %| b. rewrite Dbu Gauss_dvdl // coprime_sym in q_dv_ustar. by apply: coprimeSg coPUq; have /mulG_sub[_ sUPU] := sdprodW defPU. have c_odd: odd c by rewrite Db oddM mFT_odd andbT in b_odd. suffices /eqP c1: c == 1%N by rewrite Dbu Db c1 mul1n mulKn ?prime_gt0. rewrite eqn_leq odd_gt0 // andbT -ltnS -(odd_ltn 3) // ltnS. by rewrite -(leq_pmul2r (ltnW (ltnW qgt2))) -Db mul2n. have Db: b = (b - 1).+1 by rewrite subn1 prednK ?odd_gt0. rewrite Dbu dvdn_mulr // eqn_mod_dvd Db // -Db => /(_ isT)/dvdnP[c Db1]. have c_even: ~~ odd c by rewrite Db Db1 /= oddM mFT_odd andbT in b_odd. suffices /eqP->: b == 1%N by rewrite mul1n. have:= ub_b; rewrite Db Db1 -mul2n ltn_pmul2r ?cardG_gt0 //. by rewrite -ltnS odd_ltn //= !ltnS leqn0 => /eqP->. 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)