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