proposition: Lemma lastkey_max A (h : natmap A) x : x \in dom h -> x <= last_key h.
proof: Proof. rewrite /last_key /= !umEX; case: (UMC.from h)=>//; case=>s H _ /=. rewrite /supp /ord /= (leq_eqVlt x) orbC. by apply: sorted_last_key_maxR (sorted_oleq H)=>//; apply: otrans. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)