proposition: Lemma typeP_context : [/\ H \x 'C_U(H) = 'F(M), U^`(1)%g \subset 'C(H) /\ (U :!=: 1%g -> ~~ (U \subset 'C(H))), normedTI (cyclicTIset defW) G W & cyclicTI_hypothesis G defW].
proof: Proof. have defW2 := typeP_cent_core_compl. case: MtypeP; rewrite /= -/H => [] [cycW1 hallW1 ntW1 defM] [nilU _ _ defM']. set V := W :\: _ => [] [_ sM''F defF sFM'] [cycW2 ntW2 sW2H _ _] TI_V. have [/andP[sHM' nHM'] sUM' mulHU _ tiHU] := sdprod_context defM'. have sM'M : M' \subset M by apply: der_sub. have hallM': \pi(M').-Hall(M) M' by rewrite Hall_pi // (sdprod_Hall defM). have hallH_M': \pi(H).-Hall(M') H := pHall_subl sHM' sM'M (Fcore_Hall M). have{} defF: (H * 'C_U(H))%g = 'F(M). rewrite -(setIidPl sFM') -defF -group_modl //= -/H. rewrite setIAC (setIidPr (der_sub 1 M)). rewrite -(coprime_mulG_setI_norm mulHU) ?norms_cent //; last first. by rewrite (coprime_sdprod_Hall_l defM') (pHall_Hall hallH_M'). by rewrite mulgA (mulGSid (subsetIl _ _)). have coW12: coprime #|W1| #|W2|. rewrite coprime_sym (coprimeSg (subset_trans sW2H sHM')) //. by rewrite (coprime_sdprod_Hall_r defM). have cycW: cyclic W by rewrite (cyclic_dprod defW). have ctiW: cyclicTI_hypothesis G defW by split; rewrite ?mFT_odd. split=> //; first by rewrite dprodE ?subsetIr //= setIA tiHU setI1g. split. apply: subset_trans (_ : U :&: 'F(M) \subset _). by rewrite subsetI gFsub (subset_trans (dergS 1 sUM')). by rewrite -defF -group_modr ?subsetIl // setIC tiHU mul1g subsetIr. apply: contra => cHU; rewrite -subG1 -tiHU subsetIidr (subset_trans sUM') //. by rewrite (Fcore_max hallM') ?der_normal // -mulHU mulg_nil ?Fcore_nil. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)