proposition: Lemma umcnt_le_fresh A p (h : natmap A) t v : t <= last_key h -> um_count (predI p (le t)) (fresh h \-> v \+ h) = um_count (predI p (le t)) h.
proof: Proof. by move=>H; rewrite umcnt_fresh_le H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)