proposition: Lemma card_Syl P : p.-Sylow(G) P -> #|'Syl_p(G)| = #|G : 'N_G(P)|.
proof: Proof. by case: Sylow's_theorem P. 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)