proposition: Lemma FTtype34_noncoherence : ~ coherent (S_ H0C) M^# tau.
proof: Proof. move=> cohH0C; suff: coherent (S_ 1) M^# tau by apply: FTtype345_noncoherence. have /mulG_sub[_ sW1M] := sdprodW defM. have [nsHHU _ _ nHU tiHU] := sdprod_context defHU. have sHM: H \subset M := gFsub _ _. have [sCM sH0C_M]: C \subset M /\ H0C \subset M by rewrite !normal_sub. have nH0_C := subset_trans sCM nH0M. have sH0C_HC: H0C \subset HC by apply: genS (setSU _ _). have defF: HC :=: 'F(M) by have [/dprodWY] := typeP_context MtypeP. have{defF} nilHC: nilpotent (HC / 1) by rewrite defF quotient_nil ?Fitting_nil. have /bounded_seqIndD_coherence-bounded_coh1 := scoh1. apply: bounded_coh1 nilHC cohH0C _; rewrite ?sub1G ?normal1 //. have[_ _ /= oHbar] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5. rewrite -(index_sdprod defM) -divgS // -(dprod_card defHC) -(dprod_card defH0C). rewrite divnMr ?cardG_gt0 // divg_normal // oHbar def_p -/q. by rewrite lbound_expn_odd_prime ?mFT_odd. 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 finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10)