proposition: Lemma lastatval_freshUn v x h1 h2 : valid h1 -> [pcm h2 <= h1] -> last_atval v (fresh h1 \-> x \+ h2) = x.2.
proof: Proof. move=>V H; rewrite /last_atval /atval. rewrite lastkey_freshUn // findPtUn // valid_freshUn //. by case: H V=>h -> /validL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)