proposition: Lemma astab_gen S : S \subset R -> 'C(<<S>> | to) = 'C(S | to).
proof: Proof. move=> sSR; apply/setP=> a; case Da: (a \in D); last by rewrite !inE Da. by rewrite -!sub1set -!gacentC ?sub1set ?gen_subG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)