proposition: Lemma mset_0Vmem A : (A = mset0) + {x : K | x \in A}.
proof: Proof. have [/fsetP Aisfset0 | [a ainA]] := fset_0Vmem (finsupp A); last first. by right; exists a; rewrite -msuppE. left; apply/msetP => a; rewrite mset0E; apply/mset_eq0P. by rewrite -msuppE Aisfset0 inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap