proposition: Lemma lastatval_fresh v x h : valid h -> last_atval v (fresh h \-> x \+ h) = x.2.
proof: Proof. by move=>V; rewrite /last_atval /atval lastkey_fresh // findPtUn // valid_fresh. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)