proposition: Lemma astabCin A S : A \subset D -> (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
proof: Proof. move=> sAD; apply/subsetP/subsetP=> [sAC x xS | sSF a aA]. by apply/afixP=> a aA; apply: astab_act (sAC _ aA) xS. rewrite !inE (subsetP sAD _ aA); apply/subsetP=> x xS. by move/afixP/(_ _ aA): (sSF _ xS) => /[1!inE] ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)