proposition: Lemma umcntF p k v f : (k, v) \In f -> um_count p (free f k) = if p (k, v) then (um_count p f).-1 else um_count p f.
proof: Proof. move=>H; move/In_dom: (H)=>/= D; rewrite /um_count. case E: (k \in dom (um_filter p f)). - case/dom_umfilt: E=>w [H1 H2]. rewrite -{w H2}(In_fun H H2) in H1 *. rewrite H1 umfiltF size_domF ?subn1 //. by apply/dom_umfilt; exists v. rewrite umfiltF; case: ifP=>P; last by rewrite dom_free // E. by move/negP: E; elim; apply/dom_umfilt; exists v. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)