proposition: Lemma wordperm_iota n (p : 'S_n) : (wordperm p) =i iota 0 n.
proof: Proof. move=> i; rewrite mem_iota add0n /=. apply/idP/idP. - by move/mapP => [j _ ->] /=; apply: ltn_ord. - move=> Hi; apply/mapP; exists ((p^-1) (Ordinal Hi)). + by rewrite mem_enum. + by rewrite permKV. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp