proposition: Lemma enum_stdwordn_uniq : uniq enum_stdwordn.
proof: Proof. Proof using. by rewrite/enum_stdwordn (map_inj_uniq wordperm_inj); exact: enum_uniq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp