proposition: Corollary Hall_Jsub pi (G H K : {group gT}) : solvable G -> pi.-Hall(G) H -> K \subset G -> pi.-group K -> exists2 x, x \in G & K :^ x \subset H.
proof: Proof. move=> solG HallH sKG piK; have [x Gx sKHx] := Hall_subJ solG HallH sKG piK. by exists x^-1; rewrite ?groupV // sub_conjgV. 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)