proposition: Lemma freshPtUn h t1 v : valid h -> fresh h <= t1 -> fresh (t1 \-> v \+ h) = t1.+1.
proof: Proof. by move=>V N; rewrite /fresh lastkeyPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)