proposition: Lemma afix_comp (A : {set gT}) : A \subset B -> 'Fix_comp_action(A) = 'Fix_to(f @* A).
proof: Proof. move=> sAB; apply/setP=> x; rewrite !inE /morphim (setIidPr sAB). apply/subsetP/subsetP; first by move=> + _ /imsetP[a + ->] => /[apply]/[!inE]. by move=> + a Aa => /(_ (f a)); rewrite !inE imset_f// => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)