proposition: Lemma eval_lt_split A R a (h : natmap A) t1 t2 (z0 : R) : t1 < t2 -> eval a (lt t2) h z0 = eval a [pts k v | t1 < k < t2] h (eval a (le t1) h z0).
proof: Proof. move=>T; case V : (valid h); last first. - by move/invalidE: (negbT V)=>->; rewrite !eval_undef. rewrite eval_umfilt (umfilt_predD h (pts_sub_lt T)) evalUn; last first. - move=>x y /dom_umfilt [vx][X _] /dom_umfilt [wy][/= /andP][]. by rewrite /= -ltnNge; move/(leq_ltn_trans X). - by rewrite -(umfilt_predD h (pts_sub_lt T)) valid_umfilt. by rewrite -!eval_umfilt; apply: eq_in_eval=>kv _; apply: (ptsD_lt T). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)