proposition: Lemma acts_sum_card_orbit G S : [acts G, on S | to] -> \sum_(T in orbit to G @: S) #|T| = #|S|.
proof: Proof. by move/orbit_partition/card_partition. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)