proposition: Lemma umfilt_le_split A (h : natmap A) t1 t2 : t1 <= t2 -> um_filter (le t2) h = um_filter (le t1) h \+ um_filter [pts k _ | t1 < k <= t2] h.
proof: Proof. move=>T; rewrite -umfilt_dpredU; last first. - by case=>x y /= N; rewrite negb_and -leqNgt N. apply/eq_in_umfilt; case=>k v _ => /=. by case: (leqP k t1)=>//= /leq_trans; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)