proposition: Lemma uniq_wordperm n (p : 'S_n) : uniq (wordperm p).
proof: Proof. rewrite (eq_uniq _ (wordperm_iota p)); first exact: (iota_uniq 0 n). by rewrite size_map size_enum_ord size_iota. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp