proposition: Lemma lastatvalUn v h1 h2 : last_atval v (h1 \+ h2) = if valid (h1 \+ h2) then if last_key h1 < last_key h2 then last_atval v h2 else last_atval v h1 else v.
proof: Proof. rewrite /last_atval /atval lastkeyUn maxnC /maxn. case: ifP; last by move/negbT/invalidE=>->; rewrite find_undef. case: (ltngtP (last_key h1) (last_key h2)) => N V. - by rewrite findUnR // (dom_lastkeyE N). - by rewrite findUnL // (dom_lastkeyE N). by rewrite !(lastkeyUn0 V N) unitL lastkey0 find0E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)