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