proposition: Lemma astab_act S a x : a \in 'C(S | to) -> x \in S -> to x a = x.
proof: Proof. rewrite 2!inE => /andP[_ cSa] Sx; apply/eqP. by have /[1!inE] := subsetP cSa x Sx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)