proposition: Lemma afixS A B : A \subset B -> 'Fix_to(B) \subset 'Fix_to(A).
proof: Proof. by move=> sAB; apply/subsetP=> u /[!inE]; apply: subset_trans. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)