proposition: Lemma umcnt_mem0 p f : um_count p f = 0 <-> (forall k v, (k, v) \In f -> ~~ p (k, v)).
proof: Proof. case W : (valid f); last first. - by move/invalidE: (negbT W)=>->; rewrite umcnt_undef; split=>// _ k v /In_undef. split; first by move/(umcnt_umfilt0 W)/umfilt_mem0. by move=>H; apply/(umcnt_umfilt0 W); apply/umfilt_mem0L. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)