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