proposition: Lemma Syl_trans : [transitive G, on 'Syl_p(G) | 'JG].
proof: Proof. by case Sylow's_theorem. 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)