proposition: Lemma dom_lastkey A (h : natmap A) : valid h -> ~~ unitb h -> last_key h \in dom h.
proof: Proof. by move=>X; apply: contraR; move/(lastkey_dom X)=>->; apply/unitbP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)