proposition: Lemma setactC S a : to^* (~: S) a = ~: to^* S a.
proof: Proof. Proof using. apply/eqP; rewrite eqEcard; apply/andP; split. - apply/subsetP => x /imsetP[y]; rewrite !inE => Hy ->{x}. by move: Hy; apply contra => /imsetP[z Hz /act_inj->]. - rewrite card_setact [X in _ <= X]cardsCs setCK. by rewrite cardsCs setCK card_setact. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype div) mathcomp(finset fingroup perm morphism action)