proposition: Lemma afixP A x : reflect (forall a, a \in A -> to x a = x) (x \in 'Fix_to(A)).
proof: Proof. rewrite inE; apply: (iffP subsetP) => [xfix a /xfix | xfix a Aa]. by rewrite inE => /eqP. by rewrite inE xfix. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)