proposition: Lemma dom_lastkeyE A (h : natmap A) a : a < last_key h -> last_key h \in dom h.
proof: Proof. move=>H; case V : (valid h); last first. - by move/invalidE: (negbT V) H=>->; rewrite lastkey_undef. by apply: dom_lastkey V (contraL _ H)=>/unitbE ->; rewrite lastkey0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)