proposition: Lemma coherent_seqIndD_bound (A B C D : {group gT}) : [/\ A <| L, B <| L, C <| L & D <| L] -> [/\ A \proper K, B \subset D, D \subset C, C \subset K & D / B \subset 'Z(C / B)]%g -> coherent (S A) L^# tau -> \unless coherent (S B) L^# tau, #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R :> algC.
proof: Proof. move=> [nsAL nsBL nsCL nsDL] [ltAK sBD sDC sCK sDbZC] cohA. have sBC := subset_trans sBD sDC; have sBK := subset_trans sBC sCK. have [sAK nsBK] := (proper_sub ltAK, normalS sBK sKL nsBL). have{sBC} [nsAK nsBC] := (normalS sAK sKL nsAL, normalS sBC sCK nsBK). rewrite real_leNgt ?rpredB ?ger0_real ?mulr_ge0 ?sqrtC_ge0 ?ler0n ?ler01 //. apply/unless_contra; rewrite negbK -(Lagrange_index sKL sCK) natrM => lb_KA. pose S2 : seq 'CF(L) := [::]; pose S1 := S2 ++ S A; rewrite -[S A]/S1 in cohA. have ccsS1S: cfConjC_subset S1 calS by apply: seqInd_conjC_subset1. move: {2}_.+1 (leq_addr (size S1) (size calS).+1) => n. elim: n => [|n IHn] in (S2) S1 ccsS1S cohA * => lb_n. by rewrite ltnNge uniq_leq_size // in lb_n; case: ccsS1S. without loss /allPn[psi /= SBpsi S1'psi]: / ~~ all (mem S1) (S B). by case: allP => [sAB1 _ | _]; [apply: subset_coherent cohA | apply]. have [[_ sS1S _] Spsi] := (ccsS1S, sSS SBpsi). apply (IHn [:: psi, psi^* & S2]%CF); rewrite ?addnS 1?leqW {n lb_n IHn}//= -/S1. exact: extend_cfConjC_subset. have [phi SAphi phi1] := exists_linInd ltAK nsAK. have{SAphi} S1phi: phi \in S1 by rewrite mem_cat SAphi orbT. apply: (extend_coherent scohS) ccsS1S S1phi Spsi S1'psi _. have{SBpsi} /seqIndP[i /setDP[kBi _] {psi}->] := SBpsi; rewrite inE in kBi. rewrite {phi}phi1 cfInd1 // dvdC_mulr //; last by rewrite CintE Cnat_irr1. split; rewrite // big_cat sum_seqIndD_square // big_seq ltr_wpDl //=. apply/sumr_ge0=> xi S2xi; rewrite divr_ge0 ?cfnorm_ge0 ?exprn_ge0 //. by rewrite Cnat_ge0 // (Cnat_seqInd1 (sS1S _ _)) // mem_cat S2xi. rewrite mulrC ltr_pM2l ?gt0CiG //; apply: le_lt_trans lb_KA. by rewrite -!mulrA !ler_wpM2l ?ler0n // (irr1_bound_quo nsBC). 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)