proposition: Corollary umfilt_predC f p : f = um_filter p f \+ um_filter (predC p) f.
proof: Proof. rewrite -umfilt_dpredU; last by move=>? /=; rewrite negbK. rewrite -[LHS]umfilt_predT; apply: eq_in_umfiltE=>kv /=. by rewrite orbN. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)