proposition: Lemma perm_in_on : perm_on A perm_in.
proof: Proof. by apply/subsetP=> x; rewrite inE /= permE; case: ifP => // _; case/eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)