proposition: Lemma pgroup_fix_mod (p : nat) (G : {group aT}) (S : {set sT}) : p.-group G -> [acts G, on S | to] -> #|S| = #|'Fix_(S | to)(G)| %[mod p].
proof: Proof. move=> pG nSG; have sGD: G \subset D := acts_dom nSG. apply/eqP; rewrite -(cardsID 'Fix_to(G)) eqn_mod_dvd (leq_addr, addKn) //. have: [acts G, on S :\: 'Fix_to(G) | to]; last move/acts_sum_card_orbit <-. rewrite actsD // -(setIidPr sGD); apply: subset_trans (acts_subnorm_fix _ _). by rewrite setIS ?normG. apply: dvdn_sum => _ /imsetP[x /setDP[_ nfx] ->]. have [k oGx]: {k | #|orbit to G x| = (p ^ k)%N}. by apply: p_natP; apply: pnat_dvd pG; rewrite card_orbit_in ?dvdn_indexg. case: k oGx => [/card_orbit1 fix_x | k ->]; last by rewrite expnS dvdn_mulr. by case/afixP: nfx => a Ga; apply/set1P; rewrite -fix_x mem_orbit. 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)