proposition: Lemma lastkeyUmax h u t : last_key (upd t u h) = if t \in dom h then last_key h else if valid (upd t u h) then maxn t (last_key h) else 0.
proof: Proof. case: ifP; first by apply: lastkeyU. move=>H; rewrite validU /=; case: eqP =>[->|/eqP Nt /=]. - by rewrite upd_condN // lastkey_undef. case: ifP=>V; last first. - by move/invalidE: (negbT V)=>->; rewrite upd_undef lastkey_undef. have W : valid (upd t u h) by rewrite validU /= V Nt. have E : upd t u h = t \-> u \+ h. - apply: find_eta=>//; first by rewrite validPtUn /= V H Nt. - by move=>k; rewrite findU /= Nt V findPtUn2 // validPtUn /= Nt V H. by rewrite E lastkeyUn -E W lastkeyPt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)