proposition: Lemma nm_monoPtUn t t' (h : natmap nat) : last_key h < t -> (forall k v, (k, v) \In h -> v < t') -> um_mono (t \-> t' \+ h) = um_mono h.
proof: Proof. move=>H1 H2; case W: (valid h); last first. - by move/invalidE: (negbT W)=>->; rewrite join_undef. by apply: ummonoPtUn (lastkeyPtUn_valid _ W H1) _=>k v X; split; [move/In_dom/lastkey_max/leq_ltn_trans: X; apply|apply: H2 X]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)