proposition: Lemma out_Aut A a x : a \in Aut A -> x \notin A -> a x = x.
proof: Proof. by case/setIdP=> Aa _; apply: out_perm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)