proposition: Lemma umfilt_predU p1 p2 f : um_filter (predU p1 p2) f = um_filter p1 f \+ um_filter (predD p2 p1) f.
proof: Proof. rewrite /um_filter omap_predU /=. - apply /eq_in_omap; case=> k v H /=. by case: (p1 (k, v))=>/=; case: (p2 (k, v))=>/=. by case=> k v; case: (p1 (k, v))=>/=; [right|left]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)