proposition: Corollary Hall_superset pi (G K : {group gT}) : solvable G -> K \subset G -> pi.-group K -> exists2 H : {group gT}, pi.-Hall(G) H & K \subset H.
proof: Proof. move=> solG sKG; have [H hallH transH] := Hall_exists_subJ pi solG. by case/transH=> // x Gx sKHx; exists (H :^ x)%G; rewrite ?pHallJ. 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)