proposition: Lemma umfilt_dpredU f p q : subpred p (predC q) -> um_filter (predU p q) f = um_filter p f \+ um_filter q f.
proof: Proof. move=>D; rewrite umfilt_predU. suff : forall kv, kv \In f -> predD q p kv = q kv by move/eq_in_umfilt=>->. by move=>kv _ /=; case X: (p _)=>//=; move/D/negbTE: X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)