proposition: Lemma umfilt_predD p1 p2 f : subpred p1 p2 -> um_filter p2 f = um_filter p1 f \+ um_filter (predD p2 p1) f.
proof: Proof. move=>S; rewrite -umfilt_predU -eq_in_umfilt=>kv _ /=. by case E: (p1 _)=>//; apply: S E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)