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