proposition: Lemma Ptype_Fcore_factor_facts : [/\ C :!=: U, #|W2bar| = p & #|Hbar| = p ^ q]%N.
proof: Proof. have [defUW1 _ ntW1 _ _] := Frobenius_context Ptype_compl_Frobenius. have coHW1: coprime #|H| #|W1| := coprimegS (joing_subr U W1) coH_UW1. have [_ sUW1M _ nHUW1 _] := sdprod_context defHUW1. have nH0UW1 := subset_trans sUW1M nH0M; have [nH0U nH0W1] := joing_subP nH0UW1. have regUHb: 'C_Hbar(U / H0) = 1. have [_ sCH0] := Ptype_Fcore_kernel_exists. by rewrite -coprime_quotient_cent ?(nilpotent_sol nilH) ?quotientS1. have ->: C != U. apply: contraNneq ntHbar => defU; rewrite -subG1 -regUHb subsetIidl centsC. by rewrite -defU [C]unlock -quotient_astabQ quotientS ?subsetIr. have frobUW1b: [Frobenius U <*> W1 / H0 = (U / H0) ><| W1bar]. have tiH0UW1 := coprime_TIg (coprimeSg sH0H coH_UW1). have /isomP[inj_f im_f] := quotient_isom nH0UW1 tiH0UW1. have:= injm_Frobenius (subxx _) inj_f frobUW1. by rewrite im_f !morphim_restrm !(setIidPr _) ?joing_subl ?joing_subr. have{frobUW1b} oHbar: #|Hbar| = (#|W2bar| ^ q)%N. have nHbUW1 : U <*> W1 / H0 \subset 'N(Hbar) := quotient_norms H0 nHUW1. have coHbUW1 : coprime #|Hbar| #|U <*> W1 / H0| by apply: coprime_morph. have [//|_ _ -> //] := Frobenius_Wielandt_fixpoint frobUW1b nHbUW1 coHbUW1 _. by rewrite -(card_isog (quotient_isog _ _)) // coprime_TIg ?(coprimeSg sH0H). have abelW2bar: p.-abelem W2bar := abelemS (subsetIl _ _) abelHbar. rewrite -(part_pnat_id (abelem_pgroup abelW2bar)) p_part in oHbar *. suffices /eqP cycW2bar: logn p #|W2bar| == 1%N by rewrite oHbar cycW2bar. have cycW2: cyclic W2 by have [_ _ _ []] := MtypeP. rewrite eqn_leq -abelem_cyclic //= -/W2bar {1}defW2bar quotient_cyclic //=. rewrite lt0n; apply: contraNneq ntHbar => W2bar1. by rewrite trivg_card1 oHbar W2bar1 exp1n. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator center gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection8)