proposition: Lemma perm_undup_mset A : perm_eq (undup A) (finsupp A).
proof: Proof. apply: uniq_perm; rewrite ?undup_uniq // => a. by rewrite mem_undup msuppE. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap