proposition: Lemma enum_stdwordnE : enum_stdwordn =i is_std_of_n.
proof: Proof. Proof using. move=> /= s; apply/idP/idP. + move/mapP => [/= p _ ->]. by rewrite unfold_in /= wordperm_std /= size_map size_enum_ord. + move=> /andP[/is_std_wordpermP[p Hstd] /eqP Hsize]. apply/mapP; rewrite -Hsize; exists p; last exact Hstd. by rewrite mem_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp