proposition: Lemma umcnt_le_split A p (h : natmap A) t1 t2 : t1 <= t2 -> um_count (predI p (le t2)) h = um_count (predI p (le t1)) h + um_count (predI p [pts k v | t1 < k <= t2]) h.
proof: Proof. move=>T; rewrite -!umcnt_umfilt !(umcnt_umfiltC p). by rewrite (umcnt_predD _ (pts_sub T)) (eq_in_umcnt2 _ (ptsD T)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)