proposition: Lemma eval_fresh_le A R a (h : natmap A) t v (z0 : R) : eval a (le t) (fresh h \-> v \+ h) z0 = if t <= last_key h then eval a (le t) h z0 else if valid h then a (eval a predT h z0) (fresh h) v else z0.
proof: Proof. case V: (valid h); last first. - by move/invalidE: (negbT V)=>->; rewrite join_undef !eval_undef; case: ifP. case: ifP=>H. - by rewrite eval_umfilt umfiltPtUn valid_fresh // V ltnNge H -eval_umfilt. rewrite joinC evalUnPt; last first. - by apply/allP=>x; apply: lastkey_max. - by rewrite joinC valid_fresh. rewrite ltnNge H; congr a; apply: eq_in_eval. case=>k w /In_dom/lastkey_max /=. by case: ltngtP H=>// /ltnW H _ /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)