proposition: Lemma abelem_splits p G H : p.-abelem G -> H \subset G -> [splits G, over H].
proof: Proof. have [m] := ubnP #|G|; elim: m G H => // m IHm G H /ltnSE-leGm abelG sHG. have [-> | ] := eqsVneq H 1. by apply/splitsP; exists G; rewrite inE mul1g -subG1 subsetIl /=. case/trivgPn=> x Hx ntx; have Gx := subsetP sHG x Hx. have [_ cGG eGp] := and3P abelG. have ox: #[x] = exponent G. by apply/eqP; rewrite eqn_dvd dvdn_exponent // (abelem_order_p abelG). case/splitsP: (abelian_splits Gx ox cGG) => K; case/complP=> tixK defG. have sKG: K \subset G by rewrite -defG mulG_subr. have ltKm: #|K| < m. rewrite (leq_trans _ leGm) ?proper_card //; apply/properP; split=> //. exists x => //; apply: contra ntx => Kx; rewrite -cycle_eq1 -subG1 -tixK. by rewrite subsetI subxx cycle_subG. case/splitsP: (IHm _ _ ltKm (abelemS sKG abelG) (subsetIr H K)) => L. case/complP=> tiHKL defK; apply/splitsP; exists L; rewrite inE. rewrite -subG1 -tiHKL -setIA setIS; last by rewrite subsetI -defK mulG_subr /=. by rewrite -(setIidPr sHG) -defG -group_modl ?cycle_subG //= setIC -mulgA defK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)