proposition: Lemma lastatvalPt v p x : p != 0 -> last_atval v (p \-> x) = x.2.
proof: Proof. by move=>V; rewrite /last_atval /atval lastkeyPt // findPt /= V. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)