proposition: Lemma dom_lastkey0DX A (h : natmap A) : last_key h != 0 <-> exists k, k \in dom h.
proof: Proof. rewrite dom_lastkey0PN; split. - by case/has_nilP/hasP=>x; exists x. by case=>k D; apply/eqP=>N; rewrite N in D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)