proposition: Lemma lastkeyPtUn h t1 v : valid h -> fresh h <= t1 -> last_key (t1 \-> v \+ h) = t1.
proof: Proof. move=>V N; rewrite lastkeyPtUn_max validPtUn /= V. case: eqP N=>[->|] //= _ N. case: ifP=>D; first by rewrite /maxn; case: ltngtP N. by move/(elimF idP): D; elim; apply/negP=>/lastkey_max; case: ltngtP N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)