proposition: Lemma Sylow_Jsub P Q : p.-Sylow(G) P -> Q \subset G -> p.-group Q -> exists2 x, x \in G & Q :^ x \subset P.
proof: Proof. move=> sylP sQG pQ; have [x Gx] := Sylow_subJ sylP sQG pQ. by exists x^-1; rewrite (groupV, sub_conjgV). 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)