proposition: Lemma max_lastkey A (h : natmap A) x : x \in dom h -> {in dom h, forall y, y <= x} -> last_key h = x.
proof: Proof. rewrite /last_key !umEX; case: (UMC.from h)=>//; case=>s H _ /=. move=>H1 /= H2; apply: sorted_max_key_last (sorted_oleq H) H1 _=>//. - by apply: otrans. - by apply: oantisym. by move=>z /(H2 z); rewrite leq_eqVlt orbC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)