proposition: Lemma sub_astab1_in A x : A \subset D -> (A \subset 'C[x | to]) = (x \in 'Fix_to(A)).
proof: Proof. by move=> sAD; rewrite astabCin ?sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)