proposition: Lemma lastkey_freshX h1 h2 v : valid h1 -> valid h2 -> last_key h2 <= last_key h1 -> last_key (fresh h1 \-> v \+ h2) = fresh h1.
proof: Proof. move=>V1 V2 N; apply: max_lastkey=>[|y] /=. - by rewrite domUn inE valid_freshX //= V2 /= domPt inE /= eqxx. rewrite dom_fresh // mem_rcons inE. case/orP=>[/eqP ->//|/dom_ordfresh]. by rewrite ltnS=>H; apply: leq_trans H (ltnW _). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)