proposition: Lemma abelem_split_dprod rT p (A B : {group rT}) : p.-abelem A -> B \subset A -> exists C : {group rT}, B \x C = A.
proof: Proof. move=> abelA sBA; have [_ cAA _]:= and3P abelA. case/splitsP: (abelem_splits abelA sBA) => C /complP[tiBC defA]. by exists C; rewrite dprodE // (centSS _ sBA cAA) // -defA mulG_subr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)