proposition: Lemma p_abelem_split1 rT p (A : {group rT}) x : p.-abelem A -> x \in A -> exists B : {group rT}, [/\ B \subset A, #|B| = #|A| %/ #[x] & <[x]> \x B = A].
proof: Proof. move=> abelA Ax; have sxA: <[x]> \subset A by rewrite cycle_subG. have [B defA] := abelem_split_dprod abelA sxA. have [_ defxB _ ti_xB] := dprodP defA. have sBA: B \subset A by rewrite -defxB mulG_subr. by exists B; split; rewrite // -defxB (TI_cardMg ti_xB) mulKn ?order_gt0. 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)