proposition: Theorem SchurZassenhaus_split gT (G H : {group gT}) : Hall G H -> H <| G -> [splits G, over H].
proof: Proof. have [n] := ubnP #|G|; elim: n => // n IHn in gT G H * => /ltnSE-Gn hallH nsHG. have [sHG nHG] := andP nsHG. have [-> | [p pr_p pH]] := trivgVpdiv H. by apply/splitsP; exists G; rewrite inE -subG1 subsetIl mul1g eqxx. have [P sylP] := Sylow_exists p H. case nPG: (P <| G); last first. pose N := ('N_G(P))%G; have sNG: N \subset G by rewrite subsetIl. have eqHN_G: H * N = G by apply: Frattini_arg sylP. pose H' := (H :&: N)%G. have nsH'N: H' <| N. by rewrite /normal subsetIr normsI ?normG ?(subset_trans sNG). have eq_iH: #|G : H| = #|N| %/ #|H'|. rewrite -divgS // -(divnMl (cardG_gt0 H')) mulnC -eqHN_G. by rewrite -mul_cardG (mulnC #|H'|) divnMl // cardG_gt0. have hallH': Hall N H'. rewrite /Hall -divgS subsetIr //= -eq_iH. by case/andP: hallH => _; apply: coprimeSg; apply: subsetIl. have: [splits N, over H']. apply: IHn hallH' nsH'N; apply: {n}leq_trans Gn. rewrite proper_card // properEneq sNG andbT; apply/eqP=> eqNG. by rewrite -eqNG normal_subnorm (subset_trans (pHall_sub sylP)) in nPG. case/splitsP=> K /complP[tiKN eqH'K]. have sKN: K \subset N by rewrite -(mul1g K) -eqH'K mulSg ?sub1set. apply/splitsP; exists K; rewrite inE -subG1; apply/andP; split. by rewrite /= -(setIidPr sKN) setIA tiKN. by rewrite eqEsubset -eqHN_G mulgS // -eqH'K mulGS mulSg ?subsetIl. pose Z := 'Z(P); pose Gbar := G / Z; pose Hbar := H / Z. have sZP: Z \subset P by apply: center_sub. have sZH: Z \subset H by apply: subset_trans (pHall_sub sylP). have sZG: Z \subset G by apply: subset_trans sHG. have nZG: Z <| G by apply: gFnormal_trans nPG. have nZH: Z <| H by apply: normalS nZG. have nHGbar: Hbar <| Gbar by apply: morphim_normal. have hallHbar: Hall Gbar Hbar by apply: morphim_Hall (normal_norm _) _. have: [splits Gbar, over Hbar]. apply: IHn => //; apply: {n}leq_trans Gn; rewrite ltn_quotient //. apply/eqP=> /(trivg_center_pgroup (pHall_pgroup sylP))/eqP. rewrite trivg_card1 (card_Hall sylP) p_part -(expn0 p). by rewrite eqn_exp2l ?prime_gt1 // lognE pH pr_p cardG_gt0. case/splitsP=> Kbar /complP[tiHKbar eqHKbar]. have: Kbar \subset Gbar by rewrite -eqHKbar mulG_subr. case/inv_quotientS=> //= ZK quoZK sZZK sZKG. have nZZK: Z <| ZK by apply: normalS nZG. have cardZK: #|ZK| = (#|Z| * #|G : H|)%N. rewrite -(Lagrange sZZK); congr (_ * _)%N. rewrite -card_quotient -?quoZK; last by case/andP: nZZK. rewrite -(divgS sHG) -(Lagrange sZG) -(Lagrange sZH) divnMl //. rewrite -!card_quotient ?normal_norm //= -/Gbar -/Hbar. by rewrite -eqHKbar (TI_cardMg tiHKbar) mulKn. have: [splits ZK, over Z]. rewrite (Gaschutz_split nZZK _ sZZK) ?center_abelian //; last first. rewrite -divgS // cardZK mulKn ?cardG_gt0 //. by case/andP: hallH => _; apply: coprimeSg. by apply/splitsP; exists 1%G; rewrite inE -subG1 subsetIr mulg1 eqxx. case/splitsP=> K /complP[tiZK eqZK]. have sKZK: K \subset ZK by rewrite -(mul1g K) -eqZK mulSg ?sub1G. have tiHK: H :&: K = 1. apply/trivgP; rewrite /= -(setIidPr sKZK) setIA -tiZK setSI //. rewrite -quotient_sub1; last by rewrite subIset 1?normal_norm. by rewrite /= quotientGI //= -quoZK tiHKbar. apply/splitsP; exists K; rewrite inE tiHK ?eqEcard subxx leqnn /=. rewrite mul_subG ?(subset_trans sKZK) //= TI_cardMg //. rewrite -(@mulKn #|K| #|Z|) ?cardG_gt0 // -TI_cardMg // eqZK. by rewrite cardZK mulKn ?cardG_gt0 // Lagrange. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)