proposition: Lemma abelian_splits x G : x \in G -> #[x] = exponent G -> abelian G -> [splits G, over <[x]>].
proof: Proof. move=> Gx ox cGG; apply/splitsP; have [n] := ubnP #|G|. elim: n gT => // n IHn aT in x G Gx ox cGG * => /ltnSE-leGn. have: <[x]> \subset G by [rewrite cycle_subG]; rewrite subEproper. case/predU1P=> [<- | /properP[sxG [y]]]. by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=. have [m] := ubnP #[y]; elim: m y => // m IHm y /ltnSE-leym Gy x'y. case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]]. by rewrite -cycle_subG y1 sub1G in x'y. case x_yp: (y ^+ p \in <[x]>); last first. apply: IHm (negbT x_yp); rewrite ?groupX ?(leq_trans _ leym) //. by rewrite orderXdiv // ltn_Pdiv ?prime_gt1. have{x_yp} xp_yp: (y ^+ p \in <[x ^+ p]>). have: <[y ^+ p]>%G \in [set <[x ^+ (#[x] %/ #[y ^+ p])]>%G]. by rewrite -cycle_sub_group ?order_dvdG // inE cycle_subG x_yp eqxx. rewrite inE -cycle_subG -val_eqE /=; move/eqP->. rewrite cycle_subG orderXdiv // divnA // mulnC ox. by rewrite -muln_divA ?dvdn_exponent ?expgM 1?groupX ?cycle_id. have: p <= #[y] by rewrite dvdn_leq. rewrite leq_eqVlt => /predU1P[{xp_yp m IHm leym}oy | ltpy]; last first. case/cycleP: xp_yp => k; rewrite -expgM mulnC expgM => def_yp. suffices: #[y * x ^- k] < m. by move/IHm; apply; rewrite groupMr // groupV groupX ?cycle_id. apply: leq_ltn_trans (leq_trans ltpy leym). rewrite dvdn_leq ?prime_gt0 // order_dvdn expgMn. by rewrite expgVn def_yp mulgV. by apply: (centsP cGG); rewrite ?groupV ?groupX. pose Y := <[y]>; have nsYG: Y <| G by rewrite -sub_abelian_normal ?cycle_subG. have [sYG nYG] := andP nsYG; have nYx := subsetP nYG x Gx. have GxY: coset Y x \in G / Y by rewrite mem_morphim. have tiYx: Y :&: <[x]> = 1 by rewrite prime_TIg ?indexg1 -?[#|_|]oy ?cycle_subG. have: #[coset Y x] = exponent (G / Y). apply/eqP; rewrite eqn_dvd dvdn_exponent //. apply/exponentP=> _ /morphimP[z Nz Gz ->]. rewrite -morphX // ((z ^+ _ =P 1) _) ?morph1 //. rewrite orderE -quotient_cycle ?card_quotient ?cycle_subG // -indexgI /=. by rewrite setIC tiYx indexg1 -orderE ox -order_dvdn dvdn_exponent. case/IHn => // [||Hq]; first exact: quotient_abelian. apply: leq_trans leGn; rewrite ltn_quotient // cycle_eq1. by apply: contra x'y; move/eqP->; rewrite group1. case/complP=> /= ti_x_Hq defGq. have: Hq \subset G / Y by rewrite -defGq mulG_subr. case/inv_quotientS=> // H defHq sYH sHG; exists H. have nYX: <[x]> \subset 'N(Y) by rewrite cycle_subG. rewrite inE -subG1 eqEsubset mul_subG //= -tiYx subsetI subsetIl andbT. rewrite -{2}(mulSGid sYH) mulgA (normC nYX) -mulgA -quotientSK ?quotientMl //. rewrite -quotient_sub1 ?(subset_trans (subsetIl _ _)) // quotientIG //= -/Y. by rewrite -defHq quotient_cycle // ti_x_Hq defGq !subxx. 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)