fact: Definition seq_mset (s : seq K) := [mset[seq_mset_key] x in [fset x in s] => count (pred1 x) s].
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap