proposition: Lemma eval_le_fresh A R a (h : natmap A) t v (z0 : R) : t <= last_key h -> eval a (le t) (fresh h \-> v \+ h) z0 = eval a (le t) h z0.
proof: Proof. by move=>H; rewrite eval_fresh_le H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)