proposition: Lemma lastkey_dom A (h : natmap A) : valid h -> last_key h \notin dom h -> h = Unit.
proof: Proof. rewrite /valid /= /last_key /Unit /= !umEX /= -{4}[h]UMC.tfE. case: (UMC.from h)=>//=; case=>s H /= H1 _ /seq_last_in. rewrite /UM.empty UMC.eqE UM.umapE /supp fmapE /= {H H1}. by elim: s. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)