proposition: Lemma astabs_set1 x : 'N([set x] | to) = 'C[x | to].
proof: Proof. apply/eqP; rewrite eqEsubset astab_sub andbC setIS //. by apply/subsetP=> a; rewrite ?(inE,sub1set). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)