proposition: Lemma lastkey_freshUn h1 h2 v : valid h1 -> [pcm h2 <= h1] -> last_key (fresh h1 \-> v \+ h2) = fresh h1.
proof: Proof. move=>V [x E]; rewrite {h1}E in V *; apply: max_lastkey=>[|y] /=; rewrite domUn inE valid_freshUn // (validE2 V) /= domPt inE ?eqxx //. rewrite andbC eq_sym leq_eqVlt; case: eqP=>//= _ D. by apply: lastkey_max; 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)