proposition: Lemma lastkeyxx A (h : natmap A) : valid h -> last_key h = 0 -> h = Unit.
proof: Proof. by move=>V H; apply: lastkey_dom V _; apply/negP=>/dom_cond; rewrite H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)