proposition: Lemma umfilt_fresh V (p : pred (nat * V)) (h : natmap V) k v : fresh h <= k -> um_filter p (pts k v \+ h) = if p (k, v) then pts k v \+ um_filter p h else um_filter p h.
proof: Proof. case W : (valid h). - by move=>H; rewrite umfiltPtUn valid_fresh // W. move/negbT/invalidE: W=>->. by case: ifP; rewrite join_undef umfilt_undef // join_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)