proposition: Lemma perm_onV H s : perm_on H s -> perm_on H s^-1.
proof: Proof. move=> /subsetP sH; apply/subsetP => i /[!inE] sVi; apply: sH; rewrite inE. by apply: contra_neq sVi => si_id; rewrite -[in LHS]si_id permK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)