proposition: Lemma card_setact S a : #|to^* S a| = #|S|.
proof: Proof. by apply: card_imset; apply: act_inj. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)