proposition: Lemma cmCons v0 vn k x h : complete v0 (k \-> x \+ h) vn -> last_key h < k -> [/\ k = fresh h, vn = x.2 & complete v0 h x.1].
proof: Proof. by move=>C H; move: {C} (cmPtUn C H) (C)=>-> /cm_fresh []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)