proposition: Lemma subset_undup_step s : {subset undup s <= step s}.
proof: Proof. Proof using. by move => x; rewrite mem_undup => Hx; rewrite mem_undup mem_cat Hx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK