proposition: Lemma astab_sub S : 'C(S | to) \subset 'N(S | to).
proof: Proof. apply/subsetP=> a cSa; rewrite !inE (astab_dom cSa). by apply/subsetP=> x Sx; rewrite inE (astab_act cSa). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)