proposition: Lemma mset_eq0P {a A} : reflect (A a = 0) (a \notin A).
proof: Proof. by rewrite -mset_eq0; apply: eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap