proposition: Lemma size_mset_eq0 A : (size A == 0) = (A == mset0).
proof: Proof. apply/idP/eqP => [|->]; last by rewrite size_mset0. rewrite size_mset sum_nat_seq_eq0 => /allP AP. apply/msetP => a /=; rewrite msetE. by have /= := AP a; case: finsuppP => // _ /(_ _)/eqP->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap