proposition: Lemma dom_lastkey0P A (h : natmap A) : last_key h = 0 <-> dom h = [::].
proof: Proof. rewrite -nm_dom0; split; last first. - by case=>E; subst h; rewrite ?lastkey_undef ?lastkey0. move=>E; case V : (valid h); last by left; move/invalidE: (negbT V). right; apply: lastkey_dom=>//; rewrite E. by apply: contraT; rewrite negbK; apply: dom_cond. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)