proposition: Lemma perm_closed S s x : perm_on S s -> (s x \in S) = (x \in S).
proof: Proof. move/subsetP=> s_on_S; have [-> // | nfix_s_x] := eqVneq (s x) x. by rewrite !s_on_S // inE /= ?(inj_eq perm_inj). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)