proposition: Lemma burnside_formula : forall (gT : finGroupType) s (G : {group gT}), uniq s -> s =i G -> forall (sT : finType) (to : {action gT &-> sT}), (#|orbit to G @: setT| * size s)%N = \sum_(p <- s) #|'Fix_to[p]|.
proof: Proof. move=> gT s G Us sG sT to. rewrite big_uniq // -(card_uniqP Us) (eq_card sG) -Frobenius_Cauchy. by apply: eq_big => // p _; rewrite setTI. by apply/actsP=> ? _ ?; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)