proposition: Lemma umfilt_predX f p q : (forall kv, kv \In f -> p kv (+) q kv) -> f = um_filter p f \+ um_filter q f.
proof: Proof. move=>D; rewrite -{1}[f]umfilt_predT. have : forall kv, kv \In f -> predT kv = (predU p q) kv. - by move=>kv /D /=; case: (p kv). move/eq_in_umfilt=>->; rewrite umfilt_predU; congr (_ \+ _). by apply/eq_in_umfilt=>kv /D /=; case: (p kv)=>// /negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)