proposition: Lemma astabs_setact S a : a \in 'N(S | to) -> to^* S a = S.
proof: Proof. move=> nSa; apply/eqP; rewrite eqEcard card_setact leqnn andbT. by apply/subsetP=> _ /imsetP[x Sx ->]; rewrite astabs_act. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)