proposition: Lemma afix_subact A : A \subset subact_dom -> 'Fix_subaction(A) = val @^-1: 'Fix_to(A).
proof: Proof. move/subsetP=> sAD; apply/setP=> u. rewrite !inE !(sameP setIidPl eqP); congr (_ == A). apply/setP=> a /[!inE]; apply: andb_id2l => Aa. by rewrite -val_eqE val_subact sAD. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)