proposition: Lemma lastkeyUnf A (h1 h2 : natmap A) : valid (h1 \+ h2) -> last_key h2 <= last_key (h1 \+ h2).
proof: Proof. by rewrite joinC; apply: lastkeyfUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)