proposition: Lemma card_Syl_dvd : #|'Syl_p(G)| %| #|G|.
proof: Proof. by case Sylow_exists => P /card_Syl->; apply: dvdn_indexg. 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)