proposition: Lemma perm_of_std s : is_std s -> { p : 'S_(size s) | s = wordperm p }.
proof: Proof. rewrite /is_std => H. pose fpn := fun i : 'I_(size s) => nth 0 s i. have Hfpi i : fpn i < size s. have:= mem_nth 0 (ltn_ord i). by rewrite (perm_mem H) mem_iota /= add0n. pose fp := finfun (fun i : 'I_(size s) => Ordinal (Hfpi i)). have Hfp : injective fp. move=> i j; rewrite /fp /= !ffunE => Heq; apply/eqP. move: Heq => /(congr1 val)/eqP /=. rewrite /fpn (nth_uniq _ (ltn_ord _) (ltn_ord _)) //=. exact: std_uniq. exists (perm Hfp); rewrite /wordperm /=. apply: (@eq_from_nth _ 0); first by rewrite size_map size_enum_ord. move=> i Hi; rewrite (nth_map (Ordinal Hi)); last by rewrite size_enum_ord. rewrite -{3}[i]/(val (Ordinal Hi)). by rewrite nth_ord_enum /= permE /fp /= ffunE /= /fpn /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp