proposition: Lemma msuppE a A : (a \in finsupp A) = (a \in A).
proof: Proof. rewrite enum_msetE. apply/idP/flattenP => [aA|/=[_ /mapP[x xA -> /nseqP[->//]]]]. exists (nseq (A a) a); first by apply/mapP; exists a. by apply/nseqP; split=> //; rewrite lt0n -mem_finsupp. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap