proposition: Lemma eval_le_lt_split A R a (h : natmap A) t (z0 : R) : eval a (le t) h z0 = eval a [pts k v | k == t] h (eval a (lt t) h z0).
proof: Proof. case V : (valid h); last first. - by move/invalidE: (negbT V)=>->; rewrite !eval_undef. have D : subpred (T:=nat*A) (lt t) (le t) by case=>k v /ltnW. rewrite eval_umfilt (umfilt_predD h D) 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 D) valid_umfilt. rewrite -!eval_umfilt; apply: eq_in_eval; case=>k v _ /=. by case: ltngtP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)