proposition: Lemma umcnt_fresh_le A p (h : natmap A) t v : um_count (predI p (le t)) (fresh h \-> v \+ h) = if t <= last_key h then um_count (predI p (le t)) h else if p (fresh h, v) && valid h then 1 + um_count p h else um_count p h.
proof: Proof. case V: (valid h); last first. - move/invalidE: (negbT V)=>->; rewrite join_undef !umcnt_undef. by rewrite lastkey_undef andbF; case: ifP. case: ifP=>H. - by rewrite -!umcnt_umfilt umfiltPtUn valid_fresh // V ltnNge H. rewrite umcntPtUn ?valid_fresh //= ltnNge H /=. by rewrite umcnt_le_last; [case: ifP | case: ltngtP H]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)