proposition: Lemma wordperm_std n (p : 'S_n) : is_std (wordperm p).
proof: Proof. rewrite /is_std size_map size_enum_ord. apply: uniq_perm. - exact: uniq_wordperm. - exact: iota_uniq. - exact: wordperm_iota. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp