proposition: Lemma card_Syl_mod : prime p -> #|'Syl_p(G)| %% p = 1%N.
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)