proposition: Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) : solvable H -> K \subset 'N(H) -> K1 \subset H * K -> coprime #|H| #|K| -> #|K1| = #|K| -> exists2 x, x \in H & K1 :=: K :^ x.
proof: Proof. have [n] := ubnP #|H|. elim: n => // n IHn in gT H K K1 * => /ltnSE-leHn solH nHK. have [-> | ] := eqsVneq H 1. rewrite mul1g => sK1K _ eqK1K; exists 1; first exact: set11. by apply/eqP; rewrite conjsg1 eqEcard sK1K eqK1K /=. pose G := (H <*> K)%G. have defG: G :=: H * K by rewrite -normC // -norm_joinEl // joingC. have sHG: H \subset G by apply: joing_subl. have sKG: K \subset G by apply: joing_subr. have nsHG: H <| G by rewrite /(H <| G) sHG join_subG normG. case/(solvable_norm_abelem solH nsHG)=> M [sMH nsMG ntM] /and3P[_ abelM _]. have [sMG nMG] := andP nsMG; rewrite -defG => sK1G coHK oK1K. have nMsG (L : {set gT}): L \subset G -> L \subset 'N(M). by move/subset_trans->. have [coKM coHMK]: coprime #|M| #|K| /\ coprime #|H / M| #|K|. by apply/andP; rewrite -coprimeMl card_quotient ?nMsG ?Lagrange. have oKM (K' : {group gT}): K' \subset G -> #|K'| = #|K| -> #|K' / M| = #|K|. move=> sK'G oK'. rewrite -quotientMidr -?norm_joinEl ?card_quotient ?nMsG //; last first. by rewrite gen_subG subUset sK'G. rewrite -divgS /=; last by rewrite -gen_subG genS ?subsetUr. by rewrite norm_joinEl ?nMsG // coprime_cardMg ?mulnK // oK' coprime_sym. have [xb]: exists2 xb, xb \in H / M & K1 / M = (K / M) :^ xb. apply: IHn; try by rewrite (quotient_sol, morphim_norms, oKM K) ?(oKM K1). by apply: leq_trans leHn; rewrite ltn_quotient. by rewrite -morphimMl ?nMsG // -defG morphimS. case/morphimP=> x nMx Hx ->{xb} eqK1Kx; pose K2 := (K :^ x)%G. have{eqK1Kx} eqK12: K1 / M = K2 / M by rewrite quotientJ. suff [y My ->]: exists2 y, y \in M & K1 :=: K2 :^ y. by exists (x * y); [rewrite groupMl // (subsetP sMH) | rewrite conjsgM]. have nMK1: K1 \subset 'N(M) by apply: nMsG. have defMK: M * K1 = M <*> K1 by rewrite -normC // -norm_joinEl // joingC. have sMKM: M \subset M <*> K1 by rewrite joing_subl. have nMKM: M <| M <*> K1 by rewrite normalYl. have trMK1: M :&: K1 = 1 by rewrite coprime_TIg ?oK1K. have trMK2: M :&: K2 = 1 by rewrite coprime_TIg ?cardJg ?oK1K. apply: (Gaschutz_transitive nMKM _ sMKM) => //=; last 2 first. - by rewrite inE trMK1 defMK !eqxx. - by rewrite -!(setIC M) trMK1. - by rewrite -divgS //= -defMK coprime_cardMg oK1K // mulKn. rewrite inE trMK2 eqxx eq_sym eqEcard /= -defMK andbC. by rewrite !coprime_cardMg ?cardJg ?oK1K ?leqnn //= mulGS -quotientSK -?eqK12. 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)