proposition: Lemma gacentS : A \subset B -> 'C_(|to)(B) \subset 'C_(|to)(A).
proof: Proof. by move=> sAB; rewrite !(setIS, afixS). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)