proposition: Lemma FTtypeP_Ind_Fitting_reg_Fcore : c = 1%N.
proof: Proof. apply/eqP/wlog_neg; rewrite eqn_leq cardG_gt0 andbT -ltnNge => c_gt1. have ub_m: m < (q * (p ^ q).-1)%:R / (c * p ^ q.-1 * p.-1)%:R. rewrite 2!natrM invfM mulrACA mulrAC -natf_div ?dvdn_pred_predX // -natrM. rewrite (lt_le_trans gen_ub_m) // ler_pM ?invr_ge0 ?ler0n // leC_nat. by rewrite leq_mul //; case: Sfacts. have regCW1: semiregular C W1. have [[_ _ /Frobenius_reg_ker regUW1 _] _ _ _] := FTtypeP_facts maxS StypeP. by move=> _ y /regUW1 regUx; rewrite setIAC regUx setI1g. have{regCW1} dv_2q_c1: q.*2 %| c.-1. rewrite -(subnKC c_gt1) -mul2n Gauss_dvd ?coprime2n ?dvdn2 ?mFT_odd //=. rewrite oddB ?mFT_odd -?subSn // subn2 regular_norm_dvd_pred //. have /mulG_sub[_ sW1S] := sdprodW defS. apply: normsI; first by have [_ []] := StypeP. by rewrite (subset_trans sW1S) ?norms_cent ?gFnorm. have [q3 pge5]: q = 3%N /\ (p >= 5)%N. apply: small_m_q3; apply: (lt_le_trans ub_m). rewrite !natrM -!mulrA ler_pM2l ?gt0CG //. rewrite !invfM !mulrA -(subnKC pgt2) ler_pM2r ?invr_gt0 ?ltr0n //. rewrite ler_pdivrMr ?ltr0n ?expn_gt0 // mulrAC -natrM -expnS. rewrite prednK ?cardG_gt0 // ler_pM ?invr_ge0 ?ler0n ?leC_nat ?leq_pred //. rewrite lef_pV2 ?qualifE/= ?gt0CG ?ltr0n // leC_nat. by rewrite -(subnKC c_gt1) ltnS dvdn_leq //= -subSn ?subn2. have [_ _ [//|lb_m lb_uc]] := lb_m_cases. pose sum3 r : algC := (r.+1 ^ 2)%:R^-1 + r.+1%:R^-1 + 1. have [b Dc1] := dvdnP dv_2q_c1; rewrite q3 in Dc1. have [b0 | b_gt0] := posnP b; first by rewrite b0 -(subnKC c_gt1) in Dc1. have ub3_m r a: (r < p)%N -> (a <= b)%N -> m < 3%:R / (a * 6).+1%:R * sum3 r. move=> lb_p lb_b; apply: lt_le_trans ub_m _. rewrite !natrM !invfM mulrACA -!mulrA q3 ler_pM2l ?ltr0n //. rewrite -(ltn_predK c_gt1) Dc1 ler_pM ?mulr_ge0 ?invr_ge0 ?ler0n //. by rewrite lef_pV2 ?qualifE/= ?ltr0n // leC_nat ltnS leq_mul. rewrite predn_exp mulnC natrM 2!big_ord_recl big_ord1 /= /bump /= expn1. rewrite -(subnKC (ltnW pgt2)) add2n in lb_p *. rewrite mulfK ?pnatr_eq0 // addnA 2!natrD 2!mulrDr mulr1 {-1}natrM invfM. rewrite mulrA divfK ?mulVf ?pnatr_eq0 // lerD2r. by rewrite lerD ?lef_pV2 ?qualifE/= ?ltr0n ?leC_nat ?leq_sqr. have beq1: b = 1%N. apply: contraTeq lb_m; rewrite neq_ltn ltnNge b_gt0 => /(ub3_m 4%N) ub41. by rewrite lt_gtF // (lt_trans (ub41 _)) // /sum3 -!CratrE; compute. have c7: c = 7%N by rewrite -(ltn_predK c_gt1) Dc1 beq1. have plt11: (p < 11)%N. rewrite ltnNge; apply: contraL lb_m => /ub3_m/(_ b_gt0) ub100. by rewrite lt_gtF // (lt_trans ub100) // /sum3 -!CratrE; compute. have{plt11} p5: p = 5%N. suffices: p \in [seq r <- iota q.+1 7 | prime r & coprime r c]. by rewrite c7 q3 inE => /eqP. rewrite mem_filter mem_iota ltn_neqAle p'q q3 pgt2 pr_p (coprimeSg sW2P) //. by rewrite (coprimegS _ (Ptype_Fcore_coprime StypeP)) ?subIset ?joing_subl. have [galS | gal'S] := boolP (typeP_Galois StypeP); last first. have [H1 [_ _ _ _ []]] := typeP_Galois_Pn maxS notStype5 gal'S. case/pdivP=> r pr_r r_dv_a /(dvdn_trans r_dv_a)/idPn[]. rewrite Ptype_factor_prime // -/p p5 (Euclid_dvdM 2 2) // gtnNdvd //. rewrite odd_prime_gt2 ?(dvdn_odd (dvdn_trans r_dv_a (dvdn_indexg _ _))) //. by rewrite mFT_odd. have{galS} u_dv_31: u %| 31. have [_ _ [_ _]] := typeP_Galois_P maxS notStype5 galS. rewrite Ptype_factor_prime ?Ptype_Fcompl_kernel_cent // -/p -/q p5 q3. rewrite card_quotient // normsI ?normG ?norms_cent //. by have [] := sdprodP defPU. have hallH: Hall S H. rewrite /Hall -divgS ?gFsub //= -(sdprod_card defS) -(sdprod_card defPU). rewrite -(dprod_card defH) -mulnA divnMl ?cardG_gt0 // -/c oU mulnAC c7. have [_ [_ ->] _ _ _] := FTtypeP_facts maxS StypeP. by rewrite mulnK // -/q -/p q3 p5 coprimeMr (coprime_dvdr u_dv_31). rewrite -(leq_pmul2l (cardG_gt0 P)) muln1 (dprod_card defH) subset_leq_card //. by rewrite (Fcore_max (Hall_pi hallH)) ?gFnormal ?Fitting_nil. 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)