proposition: Lemma FTtypeP_Ind_Fitting_nonGalois_facts : ~~ typeP_Galois StypeP -> q = 3%N /\ #|U| = (p.-1./2 ^ 2)%N.
proof: Proof. have even_p1: 2 %| p.-1 by rewrite -subn1 -subSS dvdn_sub ?dvdn2 //= mFT_odd. move=> gal'S; have{gal'S} u_dv_p2q: u %| p.-1./2 ^ q.-1. have [H1 [_ _ _ _ []]] := typeP_Galois_Pn maxS notStype5 gal'S. rewrite Ptype_factor_prime ?Ptype_Fcompl_kernel_cent // -/p -/q. set a := #|U : _| => a_gt1 a_dv_p1 _ [Uhat isoUhat]. have a_odd: odd a by rewrite (dvdn_odd (dvdn_indexg _ _)) ?mFT_odd. have [_ _ nPU _] := sdprodP defPU. rewrite /u -card_quotient ?normsI ?normG ?norms_cent // (card_isog isoUhat). apply: dvdn_trans (cardSg (subsetT _)) _; rewrite cardsT card_mx mul1n. rewrite card_ord Zp_cast ?dvdn_exp2r // -(@Gauss_dvdl a _ 2) ?coprimen2 //. by rewrite -divn2 divnK. have [_ lb5_m lb3_m] := lb_m_cases. pose f r : algC := r%:R / (2 ^ r.-1)%:R. have ub_m: m < f q. apply: lt_le_trans gen_ub_m _; rewrite c1 mul1n. rewrite natrM ler_pdivrMr ?ltr0n ?expn_gt0 ?cardG_gt0 // -mulrA. rewrite ler_wpM2l ?ler0n // mulrC !natrX -expr_div_n. apply: le_trans (_ : (p.-1 %/ 2)%:R ^+ q.-1 <= _). by rewrite -natrX leC_nat divn2 dvdn_leq // expn_gt0 -(subnKC pgt2). rewrite -(subnKC qgt2) ler_pXn2r ?rpred_div ?rpred_nat // natf_div //. by rewrite ler_wpM2r ?invr_ge0 ?ler0n // leC_nat leq_pred. have{ub_m} q3: q = 3%N. apply: contraTeq ub_m; rewrite neq_ltn ltnNge qgt2 -(odd_geq 5) ?mFT_odd //=. move=> qge5; rewrite lt_gtF // -(subnKC qge5). elim: (q - 5)%N => [|r]; last apply: le_lt_trans. by apply: lt_trans (lb5_m qge5); rewrite /f -!CratrE; compute. rewrite addnS ler_pdivrMr ?ltr0n ?expn_gt0 // natrM mulrACA mulrA. by rewrite divfK ?pnatr_eq0 ?expn_eq0 // mulr_natr mulrS lerD2r ler1n. have [[]] := dvdnP u_dv_p2q; rewrite q3; first by rewrite -(subnKC pgt2). case=> [|b] Du; first by rewrite oU c1 Du muln1 mul1n. have [_ /idPn[]] := lb3_m q3; rewrite c1 divr1 le_gtF //. apply: le_trans (_ : (p.-1 ^ 2)%:R / 8%:R <= _). rewrite (natrX _ 2 3) exprSr invfM mulrA natrX -expr_div_n -natf_div // divn2. by rewrite -natrX Du ler_pdivlMr ?ltr0n // mulrC -natrM leC_nat leq_mul. rewrite -!subn1 (subn_sqr p 1) !natrM -!mulrA ler_wpM2l ?ler0n //. rewrite ler_pdivrMr 1?mulrAC ?ler_pdivlMr ?ltr0n // -!natrM leC_nat. rewrite (mulnA _ 3%N 2%N) (mulnA _ 4%N 2%N) leq_mul // mulnBl mulnDl leq_subLR. by rewrite addnCA (mulnSr p 3) -addnA leq_addr. 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)