proposition: Lemma cmPtUn v0 vn h k x : complete v0 (k \-> x \+ h) vn -> last_key h < k -> k = fresh h.
proof: Proof. by case=>V /(gpPtUn V). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)