proposition: Lemma lastkeyPtUn_valid h t u : valid h -> last_key h < t -> valid (t \-> u \+ h).
proof: Proof. move=>V L; rewrite validPtUn; apply/and3P; split=>//=. - by rewrite /= -lt0n; apply: leq_ltn_trans L. by apply: contraL L; move/lastkey_max; case: leqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)