proposition: Lemma umcnt_predDE p1 p2 f : um_count (predD p2 p1) f = um_count p2 f - um_count (predI p1 p2) f.
proof: Proof. have S1 : p2 =1 predU (predD p2 p1) (predI p1 p2). - by move=>x /=; case: (p1 x)=>//; rewrite orbF. have S2: predD (predI p1 p2) (predD p2 p1) =1 predI p1 p2. - by move=>x /=; case: (p1 x)=>//; rewrite andbF. rewrite {1}(eq_in_umcnt2 _ S1) umcnt_predU // (eq_in_umcnt2 _ S2). by rewrite -addnBA // subnn addn0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)