proposition: Lemma astab_setact_in S a : a \in D -> 'C(to^* S a | to) = 'C(S | to) :^ a.
proof: Proof. move=> Da; apply/setP=> b; rewrite mem_conjg !inE -mem_conjg conjGid //. apply: andb_id2l => Db; rewrite sub_imset_pre; apply: eq_subset_r => x. by rewrite !inE !actMin ?groupM ?groupV // invgK (canF_eq (actKVin Da)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)