proposition: Lemma out_perm S u x : perm_on S u -> x \notin S -> u x = x.
proof: Proof. by move=> uS; apply: contraNeq (subsetP uS x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)