proposition: Lemma umpleq_lastkey h1 h2 : valid h2 -> [pcm h1 <= h2] -> last_key h1 <= last_key h2.
proof: Proof. by move=>V H; case: H V=>z->V; apply: lastkey_mono=>k D; rewrite domUn inE V D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)