proposition: Lemma lastvalPX h : lastval_specx h (last_val h).
proof: Proof. case E : (last_val h)=>[a|]. - move/find_some: (E); case: dom_find=>// v /In_find H _ _. by apply: lastval_somex E H. move/find_none: E=>E. case V : (valid h). - by move/(lastkey_dom V)/(lastval_nonex V): E. by move/negbT/invalidE: V=>->; apply: lastval_undefx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)