proposition: Lemma lastvalP h : lastval_spec h (last_val h).
proof: Proof. case: lastvalPX=>[r kv|_ ->|->]. - by apply: lastval_some. - by apply: lastval_none=>[|kv /In0//]; rewrite lastval0. by apply: lastval_none=>[|kv /In_undef//]; rewrite lastval_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)