proposition: Lemma umcnt_predU p1 p2 f : um_count (predU p1 p2) f = um_count p1 f + um_count (predD p2 p1) f.
proof: Proof. case W: (valid f); last first. - by move/invalidE: (negbT W)=>->; rewrite !umcnt_undef. rewrite /um_count umfilt_predU size_domUn //. case: validUn=>//; rewrite ?(valid_umfilt,W) //. move=>k /dom_umfilt [v1 [P1 H1]] /dom_umfilt [v2 [/= P2 H2]]. by rewrite -(In_fun H1 H2) P1 in P2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)