proposition: Lemma umfilt_pt_split A (h : natmap A) k v : (k, v) \In h -> um_filter [pts x _ | k.-1 < x <= k] h = k \-> v.
proof: Proof. move=>H; have W : valid h by case: H. have N: 0 < k by move/In_dom/dom_cond: H; case: k. have subX : forall m n, 0 < n -> (m < n) = (m <= n.-1) by move=>? []. rewrite (In_eta H) umfiltPtUn -(In_eta H) /= subX // W !leqnn /=. rewrite umfilt_mem0L ?unitR ?validF //. move=>k1 v1 /InF [_ /=]; rewrite andbC; case: (ltngtP k k1) =>//=. by rewrite subX //; case: (ltngtP k1 k.-1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)