proposition: Lemma im_perm_on u S : perm_on S u -> u @: S = S.
proof: Proof. move=> Su; rewrite -preim_permV; apply/setP=> x. by rewrite !inE -(perm_closed _ Su) permKV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)