proposition: Lemma non_coherent_chief M (H1 := (K^`(1) <*> M)%G) : odd_Frobenius_quotient M -> \unless coherent (S M) L^# tau, [/\ chief_factor L H1 K /\ (#|K : H1| <= 4 * #|L : K| ^ 2 + 1)%N & exists2 p : nat, p.-group (K / M)%g /\ ~~ abelian (K / M) & ~~ (#|L : K| %| p - 1)].
proof: Proof. case=> oddL [nsML sMK nilKM]; rewrite /= -(erefl (gval H1)) => frobLb. set e := #|L : K|; have odd_e: odd e := dvdn_odd (dvdn_indexg L K) oddL. have{odd_e} mod1e_lb m: odd m -> m == 1 %[mod e] -> (m > 1 -> 2 * e + 1 <= m)%N. move=> odd_m e_dv_m1 m_gt1; rewrite eqn_mod_dvd 1?ltnW // subn1 in e_dv_m1. by rewrite mul2n addn1 dvdn_double_ltn. have nsH1L: H1 <| L by rewrite normalY // gFnormal_trans. have nsH1K: H1 <| K by rewrite (normalS _ sKL nsH1L) // join_subG der_sub. have [sH1K nH1K] := andP nsH1K; have sMH1: M \subset H1 by apply: joing_subr. have cohH1: coherent (S H1) L^# tau. apply: uniform_degree_coherence (subset_subcoherent scohS _) _ => //. apply/(@all_pred1_constant _ e%:R)/allP=> _ /mapP[chi Schi ->] /=. have [i /setIdP[_]] := seqIndP Schi; rewrite inE join_subG -lin_irr_der1. by case/andP=> lin_chi _ ->; rewrite cfInd1 ?lin_char1 ?mulr1. apply/unlessP; have [/val_inj-> | ltMH1] := eqVproper sMH1; first by left. have [lbK|ubK] := ltnP; [by left; apply: bounded_seqIndD_coherence lbK | right]. have{} ubK: (#|K : H1| < (2 * e + 1) ^ 2)%N. apply: leq_ltn_trans ubK _; rewrite -subn_gt0 sqrnD expnMn addKn. by rewrite !muln_gt0 indexg_gt0. have{frobLb} [[E1b frobLb] [sH1L nH1L]] := (existsP frobLb, andP nsH1L). have [defLb ntKb _ _ /andP[sE1L _]] := Frobenius_context frobLb. have iH1_mod1e H2: H1 \subset H2 -> H2 \subset K -> L \subset 'N(H2) -> #|H2 : H1| == 1 %[mod e]. - move=> sH12 sH2K nPL; have sH2L := subset_trans sH2K sKL. rewrite eqn_mod_dvd // subn1 -card_quotient ?(subset_trans sH2L) //. have [-> | ntH2b] := eqVneq (H2 / H1)%g 1%g; first by rewrite cards1. have ->: e = #|E1b|. by rewrite (index_sdprod defLb) index_quotient_eq ?(setIidPr sH1L). have /Frobenius_subl/Frobenius_dvd_ker1-> := frobLb; rewrite ?quotientS //. by rewrite (subset_trans sE1L) ?quotient_norms. have{iH1_mod1e} chiefH1: chief_factor L H1 K. have ltH1K: H1 \proper K by rewrite /proper sH1K -quotient_sub1 ?subG1. rewrite /chief_factor nsKL andbT; apply/maxgroupP; rewrite ltH1K. split=> // H2 /andP[ltH2K nH2L] sH12; have sH2K := proper_sub ltH2K. have /eqVproper[// | ltH21] := sH12; case/idPn: ubK; rewrite -leqNgt. have iKH1: (#|K : H2| * #|H2 : H1|)%N = #|K : H1| by apply: Lagrange_index. have iH21_mod1e: #|H2 : H1| == 1 %[mod e] by apply/iH1_mod1e. have iKH1_mod1e: #|K : H1| = 1 %[mod e] by apply/eqP/iH1_mod1e. have iKH2_mod1e: #|K : H2| == 1 %[mod e]. by rewrite -iKH1_mod1e -iKH1 -modnMmr (eqP iH21_mod1e) modnMmr muln1. have odd_iK := dvdn_odd (dvdn_indexg _ _) (oddSg (subset_trans _ sKL) oddL). by rewrite -iKH1 leq_mul ?mod1e_lb ?odd_iK ?indexg_gt1 ?proper_subn. have nMK: K \subset 'N(M) := subset_trans sKL (normal_norm nsML). have nMK1: K^`(1)%g \subset 'N(M) by apply: gFsub_trans. have not_abKb: ~~ abelian (K / M). apply: contra (proper_subn ltMH1) => /derG1P/trivgP/=. by rewrite join_subG subxx andbT -quotient_der ?quotient_sub1. have /is_abelemP[p p_pr /and3P[pKb _ _]]: is_abelem (K / H1). have: solvable (K / H1)%g by apply: quotient_sol solK. by case/(minnormal_solvable (chief_factor_minnormal chiefH1)). have [[_ p_dv_Kb _] nsMK] := (pgroup_pdiv pKb ntKb, normalS sMK sKL nsML). have isoKb: K / M / (H1 / M) \isog K / H1 := third_isog sMH1 nsMK nsH1K. have{nilKM} pKM: p.-group (K / M)%g. pose Q := 'O_p^'(K / M); have defKM: _ \x Q = _ := nilpotent_pcoreC p nilKM. have nH1Q: Q \subset 'N(H1 / M) by rewrite gFsub_trans ?quotient_norms. have hallQb := quotient_pHall nH1Q (nilpotent_pcore_Hall p^' nilKM). have{nH1Q hallQb pKb} sQH1: (Q \subset H1 / M)%g. rewrite -quotient_sub1 // subG1 trivg_card1 /= (card_Hall hallQb). by rewrite partG_eq1 pgroupNK (isog_pgroup p isoKb). suffices Q_1: Q = 1%g by rewrite -defKM Q_1 dprodg1 pcore_pgroup. apply: contraTeq sQH1 => ntQ; rewrite quotientYidr ?quotient_der //. rewrite (sameP setIidPl eqP) -(dprod_modr (der_dprod 1 defKM)) ?gFsub //= -/Q. rewrite setIC coprime_TIg ?(coprimeSg (der_sub 1 _)) ?coprime_pcoreC //. by rewrite dprod1g proper_neq ?(sol_der1_proper (nilpotent_sol nilKM)) ?gFsub. split=> //; exists p => //; apply: contra not_abKb => e_dv_p1. rewrite cyclic_abelian // Phi_quotient_cyclic //. have /homgP[f <-]: (K / M / 'Phi(K / M) \homg K / H1)%g. apply: homg_trans (isog_hom isoKb). rewrite homg_quotientS ?gFnorm ?quotient_norms //= quotientYidr //. by rewrite quotient_der // (Phi_joing pKM) joing_subl. rewrite {f}morphim_cyclic // abelian_rank1_cyclic; last first. by rewrite sub_der1_abelian ?joing_subl. rewrite (rank_pgroup pKb) (leq_trans (p_rank_le_logn _ _)) //. rewrite -ltnS -(ltn_exp2l _ _ (prime_gt1 p_pr)) -p_part part_pnat_id //. rewrite card_quotient // (leq_trans ubK) // leq_exp2r //. have odd_p: odd p by rewrite (dvdn_odd p_dv_Kb) ?quotient_odd ?(oddSg sKL). by rewrite mod1e_lb ?eqn_mod_dvd ?prime_gt0 ?prime_gt1. 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)