proposition: Lemma ext_coprime_Hall_subset (X : {group gT}) : X \subset G -> pi.-group X -> [acts A, on X | to] -> exists H : {group gT}, [/\ pi.-Hall(G) H, [acts A, on H | to] & X \subset H].
proof: Proof. move=> sXG piX; rewrite actsEsd // => nXA'. case: (coprime_Hall_subset nGA' coGA' solG' _ (morphim_pgroup _ piX) nXA'). exact: morphimS. move=> H' /= [piH' nHA' sXH']; have sHG' := pHall_sub piH'. exists (inG @*^-1 H')%G; rewrite actsEsd ?subsetIl ?morphpreK // nHA'. rewrite -sub_morphim_pre //= sXH'; split=> //. by rewrite -(morphim_invmE injG) -{1}(im_invm injG) morphim_pHall. 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)