proposition: Lemma mset_seqE s a : (seq_mset s) a = count_mem a s.
proof: Proof. by rewrite fsfunE inE/=; case: ifPn => // /count_memPn ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap