proposition: Lemma wordperm_invP n (p : 'S_n) i (j : 'I_n) : nth n (wordperm p) i = j <-> i = (p^-1) j.
proof: Proof. split; rewrite /wordperm. - case (ltnP i n) => Hi. + rewrite (nth_map j); last by rewrite size_enum_ord. rewrite /= => /val_inj <-. by rewrite permK nth_enum_ord. + rewrite nth_default; last by rewrite size_map size_enum_ord. by move=> Hn; exfalso; have:= ltn_ord j; rewrite -{1}Hn ltnn. - move ->; rewrite (nth_map j); last by rewrite size_enum_ord; apply: ltn_ord. by rewrite nth_ord_enum /= permKV. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp