proposition: Lemma umcnt_pred0 f : um_count pred0 f = 0.
proof: Proof. case W : (valid f); last first. - by move/invalidE: (negbT W)=>->; rewrite umcnt_undef. by rewrite /um_count umfilt_pred0 // dom0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)