proposition: Lemma astabs_act S a x : a \in 'N(S | to) -> (to x a \in S) = (x \in S).
proof: Proof. rewrite 2!inE subEproper properEcard => /andP[_]. rewrite (card_preimset _ (act_inj _)) ltnn andbF orbF => /eqP{2}->. by rewrite inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)