proposition: Lemma Sylow_trans P Q : p.-Sylow(G) P -> p.-Sylow(G) Q -> exists2 x, x \in G & Q :=: P :^ x.
proof: Proof. move=> sylP sylQ; have /[!inE] := (atransP2 Syl_trans) P Q. by case=> // x Gx ->; 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)