proposition: Theorem Maschke_abelem gT p (G V U : {group gT}) : p.-abelem V -> p^'.-group G -> U \subset V -> G \subset 'N(V) -> G \subset 'N(U) -> exists2 W : {group gT}, U \x W = V & G \subset 'N(W).
proof: Proof. move=> pV p'G sUV nVG nUG. have splitU: [splits V, over U] := abelem_splits pV sUV. case/and3P: pV => pV abV; have cUV := subset_trans sUV abV. have sVVG := joing_subl V G. have{nUG} nUVG: U <| V <*> G. by rewrite /(U <| _) join_subG (subset_trans sUV) // cents_norm // centsC. rewrite -{nUVG}(Gaschutz_split nUVG) ?(abelianS sUV) // in splitU; last first. rewrite -divgS ?joing_subl //= norm_joinEr //. have coVG: coprime #|V| #|G| := pnat_coprime pV p'G. by rewrite coprime_cardMg // mulnC mulnK // (coprimeSg sUV). case/splitsP: splitU => WG /complP[tiUWG /= defVG]. exists (WG :&: V)%G. rewrite dprodE; last by rewrite setIA tiUWG (setIidPl _) ?sub1G. by rewrite group_modl // defVG (setIidPr _). by rewrite subIset // orbC centsC cUV. rewrite (subset_trans (joing_subr V _)) // -defVG mul_subG //. by rewrite cents_norm ?(subset_trans cUV) ?centS ?subsetIr. rewrite normsI ?normG // (subset_trans (mulG_subr U _)) //. by rewrite defVG join_subG normG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)