proposition: Lemma perm_bound (x : word) (s : seq word) : all (perm_eq x) s -> uniq s -> size s <= (size x)`!.
proof: Proof. Proof using. by rewrite -(size_permuted_seq x); apply: full_bound; exact: eq_seqE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK