proposition: Lemma umcnt_umfilt0 f : valid f -> forall p, um_count p f = 0 <-> um_filter p f = Unit.
proof: Proof. move=>W; split; last by rewrite /um_count=>->; rewrite dom0. by move/size0nil=>D; apply: dom0E; rewrite ?valid_umfilt ?D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)