proposition: Lemma lastkeyUn h1 h2 : last_key (h1 \+ h2) = if valid (h1 \+ h2) then maxn (last_key h1) (last_key h2) else 0.
proof: Proof. have H (k1 k2 : natmap A) : valid (k1 \+ k2) -> last_key k1 < last_key k2 -> last_key (k1 \+ k2) = last_key k2. - move=>V H; apply: max_lastkey=>[|x]. - by rewrite domUn inE V (dom_lastkeyE H) orbT. rewrite domUn inE V; case/orP; move/lastkey_max=>// T; by apply: leq_trans T (ltnW H). case V : (valid _); last first. - by move/invalidE: (negbT V)=>->; rewrite lastkey_undef. rewrite /maxn; case: (ltngtP (last_key h2) (last_key h1)). - by rewrite joinC in V *; apply: H. - by apply: H. by move/esym/(lastkeyUn0 V)=>E; rewrite !E unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)