proposition: Lemma eval_le_last A R a (h : natmap A) t (z0 : R) : last_key h <= t -> eval a (le t) h z0 = eval a xpredT h z0.
proof: Proof. by move=>H; apply: eq_in_eval; case=>k v /In_dom/lastkey_max/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)