proposition: Lemma wordperm_inj : injective (@wordperm n).
proof: Proof. Proof using. move=> p q; rewrite /wordperm => Heq. rewrite -permP => i; have:= congr1 (fun s => nth 0 s i) Heq. have Hi : i < size (enum 'I_n) by rewrite size_enum_ord; apply: ltn_ord. rewrite /= !(nth_map i _ _ Hi). by rewrite nth_ord_enum; exact: val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp