proposition: Lemma cmPt v0 vn k x : complete v0 (k \-> x) vn -> k = 1 /\ x = (v0, vn).
proof: Proof. case; rewrite validPt; case: k=>//= k _ /(_ 1). rewrite lastkeyPt //= domPt inE /= => /(_ (erefl _))/eqP ->. move/(_ 0 x); rewrite findPt findPt2 /= => -> //. by rewrite /last_atval lastkeyPt // /atval findPt /= => <-; case: x. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)