proposition: Lemma Hall_psubJ p pi G H P : pi.-Hall(G) H -> p \in pi -> P \subset G -> p.-group P -> exists2 x, x \in G & P \subset H :^ x.
proof: Proof. move=> hallH pi_p sPG pP; have [x Gx sPxH] := Hall_pJsub hallH pi_p sPG pP. by exists x^-1; rewrite ?groupV -?sub_conjg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)