proposition: Lemma umcnt_umfiltU p f q1 q2 : um_count p (um_filter (predU q1 q2) f) = um_count p (um_filter q1 f) + um_count p (um_filter (predD q2 q1) f).
proof: Proof. rewrite umcnt_umfiltC umcnt_predU ?valid_umfilt //. by rewrite !(umcnt_umfiltC p). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)