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