proposition: Lemma range_freshUnK (A : ordType) (h : natmap A) k (v : A) : valid h -> last_key h < k -> range (k \-> v \+ h) = rcons (range h) v.
proof: Proof. move=>V K; rewrite joinC rangeUnPtK //; last first. - by apply/allP=>x /lastkey_max/leq_ltn_trans; apply. rewrite validUnPt V /=; case: k K=>//= k K. by apply: contraL K=>/lastkey_max; rewrite ltnS; case: ltngtP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)