proposition: Lemma astab1_set S : 'C[S | set_action] = 'N(S | to).
proof: Proof. apply/setP=> a; apply/idP/idP=> nSa. case/setIdP: nSa => Da; rewrite !inE Da sub1set inE => /eqP defS. by apply/subsetP=> x Sx; rewrite inE -defS mem_setact. by rewrite !inE (astabs_dom nSa) sub1set inE /= astabs_setact. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)