proposition: Lemma astab_setact S a : 'C(to^* S a | to) = 'C(S | to) :^ a.
proof: Proof. apply/setP=> b; rewrite mem_conjg. apply/astabP/astabP=> stab x => [Sx|]. by rewrite conjgE invgK !actM stab ?actK //; apply/imsetP; exists x. by case/imsetP=> y Sy ->{x}; rewrite -actM conjgCV actM stab. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)