proposition: Theorem bounded_seqIndD_coherence M H H1 : [/\ M <| L, H <| L & H1 <| L] -> [/\ M \subset H1, H1 \subset H & H \subset K] -> nilpotent (H / M) -> coherent (S H1) L^# tau -> (#|H : H1| > 4 * #|L : K| ^ 2 + 1)%N -> coherent (S M) L^# tau.
proof: Proof. move: H1 => A [nsML nsHL nsAL] [sMA sAH sHK] nilHb cohA lbHA. elim: {A}_.+1 {-2}A (ltnSn #|A|) => // m IHm A leAm in nsAL sMA sAH cohA lbHA *. have [/group_inj-> // | ltMA] := eqVproper sMA; have [sAL nAL] := andP nsAL. have{ltMA} [B maxB sMB]: {B : {group gT} | maxnormal B A L & M \subset B}. by apply: maxgroup_exists; rewrite ltMA normal_norm. have /andP[ltBA nBL] := maxgroupp maxB; have [sBA not_sAB] := andP ltBA. have [sBH sBL] := (subset_trans sBA sAH, subset_trans sBA sAL). have nsBL: B <| L by apply/andP. suffices{m IHm leAm} cohB: coherent (S B) L^# tau. apply: IHm cohB _ => //; first exact: leq_trans (proper_card ltBA) _. by rewrite (leq_trans lbHA) // dvdn_leq // indexgS. have /andP[sHL nHL] := nsHL. have sAbZH: (A / B \subset 'Z(H / B))%g. have nBA := subset_trans sAL nBL; have nsBA : B <| A by apply/andP. set Zbar := 'Z(H / B); set Abar := (A / B)%g; pose Lbar := (L / B)%g. have nZHbar: Lbar \subset 'N(Zbar) by rewrite gFnorm_trans ?quotient_norms. have /mingroupP[/andP[ntAbar nALbar] minBbar]: minnormal Abar Lbar. apply/mingroupP; split=> [|Dbar /andP[ntDbar nDLbar] sDAbar]. by rewrite -subG1 quotient_sub1 // not_sAB quotient_norms. have: Dbar <| Lbar by rewrite /normal (subset_trans sDAbar) ?quotientS. case/(inv_quotientN nsBL)=> D defDbar sBD /andP[sDL nDL]. apply: contraNeq ntDbar => neqDAbar; rewrite defDbar quotientS1 //. have [_ /(_ D) {1}<- //] := maxgroupP maxB. rewrite -(quotient_proper (normalS sBD sDL nsBL)) // -defDbar. by rewrite properEneq sDAbar neqDAbar. apply/setIidPl/minBbar; rewrite ?subsetIl {minBbar}//= andbC -/Abar -/Zbar. rewrite normsI ?meet_center_nil ?quotient_normal ?(normalS sAH sHL) //=. suffices /homgP[f /= <-]: (H / B)%g \homg (H / M)%g by rewrite morphim_nil. by apply: homg_quotientS; rewrite ?(subset_trans sHL) ?normal_norm. have ltAH: A \proper H. by rewrite properEneq sAH (contraTneq _ lbHA) // => ->; rewrite indexgg addn1. set x : algC := sqrtC #|H : A|%:R. have [nz_x x_gt0]: x != 0 /\ 0 < x by rewrite gt_eqF sqrtC_gt0 gt0CiG. without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2%:R * #|L : H|%:R * x. have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK). exact: coherent_seqIndD_bound id. suffices{lbHA}: (x - x^-1) ^+ 2 <= (2 * #|L : K|)%:R ^+ 2. rewrite lt_geF // sqrrB divff // sqrtCK ltr_pwDr ?exprn_gt0 ?invr_gt0 //. by rewrite lerBrDr -natrX -natrD ler_nat expnMn addnS lbHA. rewrite ler_pXn2r ?unfold_in /= ?ler0n //; last first. by rewrite subr_ge0 -div1r ler_pdivrMr // -expr2 sqrtCK ler1n. rewrite -(ler_pM2l x_gt0) -(ler_pM2l (gt0CiG K H)) 2!mulrBr -expr2 sqrtCK. rewrite !mulrA mulfK // mulrAC natrM mulrCA -2!natrM [in _ * x]mulnC. by rewrite !Lagrange_index // (le_trans _ ubKA) // lerD2l lerN2 ler1n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator gseries nilpotent) mathcomp(sylow abelian maximal hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC algnum) mathcomp(classfun character inertia vcharacter integral_char) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)