proposition: Lemma umcnt_filt_eq p f : um_count p f = size (dom f) <-> f = um_filter p f.
proof: Proof. rewrite umcnt_memT -{2}[f]umfilt_predT -eq_in_umfilt. by split=>H; [case=>k v /H | move=>k v /H]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)