proposition: Lemma astabsC S : 'N(~: S | to) = 'N(S | to).
proof: Proof. apply/setP=> a; apply/idP/idP=> nSa; rewrite !inE (astabs_dom nSa). by rewrite -setCS -preimsetC; apply/subsetP=> x; rewrite inE astabs_act. by rewrite preimsetC setCS; apply/subsetP=> x; rewrite inE astabs_act. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)