proposition: Lemma FT_Frobenius_coherence : {subset calS <= irr L} /\ coherent calS L^# tau.
proof: Proof. have irrS: {subset calS <= irr L}. by move=> _ /seqIndC1P[s nz_s ->]; apply: irr_induced_Frobenius_ker. split=> //; have [U [MtypeF MtypeI]] := FTtypeP 1 maxL Ltype1. have [[ntH ntU defL] _ _] := MtypeF; have nsHL: H <| L := gFnormal _ L. have nilH: nilpotent H := Fcore_nil L; have solH := nilpotent_sol nilH. have frobHU: [Frobenius L = H ><| U] := set_Frobenius_compl defL frobL. have [R [scohS _ _]] := Rgen maxL Ltype1; rewrite -/calS -/tau in scohS. have [tiH | [cHH _] | [expUdvH1 _]] := MtypeI. - have /Sibley_coherence := And3 (mFT_odd L) nilH tiH. case/(_ U)=> [|tau1 [IZtau1 Dtau1]]; first by left. exists tau1; split=> // chi Schi; rewrite Dtau1 //. by rewrite /tau Dade_Ind ?FTsupp_Frobenius ?(zcharD1_seqInd_on _ Schi). - apply/(uniform_degree_coherence scohS)/(@all_pred1_constant _ #|L : H|%:R). apply/allP=> _ /mapP[_ /seqIndP[s _ ->] ->] /=. by rewrite cfInd1 ?gFsub // lin_char1 ?mulr1 //; apply/char_abelianP. apply: (non_coherent_chief _ _ scohS) id _ => // [|[_ [p [pH _] /negP[]]]]. split; rewrite ?mFT_odd ?normal1 ?sub1G ?quotient_nil //= joingG1. apply/existsP; exists (U / H')%G. by rewrite Frobenius_proper_quotient ?(sol_der1_proper solH) ?gFnormal_trans. rewrite subn1 -(index_sdprod defL) -(isog_pgroup p (quotient1_isog H)) in pH *. have /expUdvH1: p \in \pi(H) by rewrite -p_part_gt1 part_pnat_id ?cardG_gt1. by have [-> //] := typeF_context MtypeF; split; rewrite ?(sdprodWY defL). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg 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 mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)