proposition: Lemma umcnt_eval0 R a p f (z0 : R) : um_count p f = 0 -> eval a p f z0 = z0.
proof: Proof. case W : (valid f); last first. - by move/invalidE: (negbT W)=>->; rewrite eval_undef. by move/(umcnt_umfilt0 W)=>E; rewrite eval_umfilt E eval0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)