proposition: Lemma FTtypeP_Ind_Fitting_Galois_ub b : (p ^ q).-1 %/ p.-1 = (b * u)%N -> (b <= q.*2)%N.
proof: Proof. move=> Dbu; have: U :!=: 1%g by have [[_ _ /Frobenius_context[]]] := Sfacts. rewrite trivg_card1 oU c1 muln1 leqNgt; apply: contra => bgt2q. have [|q3 pge5] := small_m_q3. apply: lt_le_trans gen_ub_m _; rewrite c1 mul1n !natrM -!mulrA. rewrite ler_wpM2l ?ler0n // ler_pdivrMr ?ltr0n ?expn_gt0 ?cardG_gt0 //. rewrite mulrAC invfM -natrM -expnS prednK ?cardG_gt0 // mulrCA. rewrite ler_pdivlMl ?ltr0n // -natrM. apply: le_trans (_ : (b * u)%:R <= _); first by rewrite leC_nat leq_mul. rewrite -Dbu natf_div ?dvdn_pred_predX // ler_wpM2r ?invr_ge0 ?ler0n //. by rewrite leC_nat leq_pred. have ub_p: ((p - 3) ^ 2 < 4 ^ 2)%N. have [_ _ [] // _] := lb_m_cases; rewrite c1 divr1 ltr_pdivrMr ?ltr0n //. rewrite -natrM ltC_nat prednK ?expn_gt0 ?cardG_gt0 // => /(leq_mul bgt2q). rewrite mulnC mulnA -Dbu q3 predn_exp mulKn; last by rewrite -(subnKC pgt2). rewrite 2!big_ord_recl big_ord1 /= /bump /= !mulnDl expn0 expn1. rewrite addnA mulnS leq_add2r -(leq_add2r 9) (mulnCA p 2%N 3%N) -addnA addnCA. by rewrite -leq_subLR -(sqrnB pgt2). have{ub_p pge5} p5: p = 5%N. apply/eqP; rewrite eqn_leq pge5 andbT. by rewrite ltn_sqr ltnS leq_subLR -ltnS odd_ltn ?mFT_odd in ub_p. have bgt1: (1 < b)%N by rewrite -(subnKC bgt2q) q3. rewrite -(eqn_pmul2l (ltnW bgt1)) muln1 eq_sym. by apply/eqP/prime_nt_dvdP; rewrite ?dvdn_mulr ?gtn_eqF // -Dbu q3 p5. 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)