proposition: Lemma lastkeyPtUn_max h t u : last_key (t \-> u \+ h) = if valid (t \-> u \+ h) then maxn t (last_key h) else 0.
proof: Proof. by rewrite lastkeyUn; case: ifP=>// /validPtUn_cond /= D; rewrite lastkeyPt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)