proposition: Lemma ext_coprime_Hall_exists : exists2 H : {group gT}, pi.-Hall(G) H & [acts A, on H | to].
proof: Proof. have [H' hallH' nHA'] := coprime_Hall_exists pi nGA' coGA' solG'. have sHG' := pHall_sub hallH'. exists (inG @*^-1 H')%G => /=. by rewrite -(morphim_invmE injG) -{1}(im_invm injG) morphim_pHall. by rewrite actsEsd ?morphpreK // subsetIl. 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)