proposition: Lemma lastkey_fresh h v : valid h -> last_key (fresh h \-> v \+ h) = fresh h.
proof: Proof. move=>Vf; apply: max_lastkey=>[|x] /=. - by rewrite domUn inE valid_fresh // Vf domPt inE eqxx. rewrite domUn inE /= valid_fresh // Vf /= domPt inE /= eq_sym. by rewrite leq_eqVlt; case: eqP=>//= _; apply: dom_ordfresh. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)