proposition: Lemma umcnt_count q f : count q (dom f) = um_count (q \o fst) f.
proof: Proof. rewrite assocs_dom /um_count -size_assocs. by rewrite assocs_umfilt /= size_filter count_map. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)