proposition: Theorem Frobenius_Cauchy G S : [acts G, on S | to] -> \sum_(a in G) #|'Fix_(S | to)[a]| = (#|orbit to G @: S| * #|G|)%N.
proof: Proof. move=> GactS; have sGD := acts_dom GactS. transitivity (\sum_(a in G) \sum_(x in 'Fix_(S | to)[a]) 1%N). by apply: eq_bigr => a _; rewrite -sum1_card. rewrite (exchange_big_dep [in S]) /= => [|a x _]; last by case/setIP. rewrite (set_partition_big _ (orbit_partition GactS)) -sum_nat_const /=. apply: eq_bigr => _ /imsetP[x Sx ->]. rewrite -(card_orbit_in_stab x sGD) -sum_nat_const. apply: eq_bigr => y; rewrite orbit_in_sym // => /imsetP[a Ga defx]. rewrite defx astab1_act_in ?(subsetP sGD) //. rewrite -{2}(conjGid Ga) -conjIg cardJg -sum1_card setIA (setIidPl sGD). by apply: eq_bigl => b; rewrite !(sub1set, inE) -(acts_act GactS Ga) -defx Sx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)