proposition: Lemma pprod_trans_coprime g : g \in G -> H :^ g \subset U -> exists2 c, c \in 'C_K(H) & exists2 u, u \in U & g = c * u.
proof: Proof. rewrite -{1}defG => /mulsgP[k u Kk Uu defg] sHgU. have [sK_KH sH_KH] := joing_sub (erefl (K <*> H)). have hallH: \pi(H).-Hall(K <*> H :&: U) H. rewrite (pHall_subl _ (subsetIl _ _)) ?subsetI ?sH_KH //. rewrite /pHall sH_KH pgroup_pi /= joingC norm_joinEl // indexMg -indexgI. by rewrite -coprime_pi' ?cardG_gt0 //= coprime_sym coprime_TIg ?indexg1. have{sHgU} hallHk: \pi(H).-Hall(K <*> H :&: U) (H :^ k). rewrite pHallE cardJg (card_Hall hallH) eqxx andbT subsetI andbC. rewrite -(conjSg _ _ u) (conjGid Uu) -conjsgM -defg sHgU. by rewrite sub_conjg conjGid // groupV (subsetP sK_KH). have{hallH hallHk} [w KUw defHk]: exists2 w, w \in K :&: U & H :^ k = H :^ w. have sKHU_G: K <*> H :&: U \subset G by rewrite setIC subIset ?sUG. have [hw KHUhw ->] := Hall_trans (solvableS sKHU_G solG) hallHk hallH. have: hw \in H * (K :&: U) by rewrite group_modl // -norm_joinEl // joingC. by case/mulsgP=> h w Hh KUw ->; exists w; rewrite // conjsgM (conjGid Hh). have{KUw} [Kw Uw] := setIP KUw. exists (k * w^-1); last by exists (w * u); rewrite ?groupM // -mulgA mulKg. by rewrite -coprime_norm_cent // !inE groupM ?groupV //= conjsgM defHk conjsgK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)