proposition: Lemma mset_eq0 a A : (A a == 0) = (a \notin A).
proof: Proof. by rewrite -mset_neq0 negbK. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap