proposition: Lemma umcntU p k v w f : (k, w) \In f -> um_count p (upd k v f) = if p (k, v) then if p (k, w) then um_count p f else (um_count p f).+1 else if p (k, w) then (um_count p f).-1 else um_count p f.
proof: Proof. move=>H; have E : f = pts k w \+ free f k. - by apply: um_eta2; apply/In_find. have W1 : valid f by move/In_dom/dom_valid: H. have W2 : valid (pts k v \+ free f k). - by rewrite {1}E !validPtUn in W1 *. have W3 : valid (pts k w \+ free f k). - by rewrite {1}E !validPtUn in W1 *. rewrite {1}E updPtUn umcntPtUn // (umcntF p H). case: ifP=>H1; case: ifP=>H2; rewrite ?add0n ?add1n //. have: um_count p f > 0; first by rewrite E umcntPtUn // H2. by case X: (um_count p f). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)