proposition: Lemma fresh_lt V (h : natmap V) x : fresh h <= x -> um_filterk [ pred k | k < x ] h = h.
proof: Proof. move=>F; rewrite -[RHS]umfilt_predT. apply/eq_in_umfilt; case=>y v /In_dom/lastkey_max /= K. by rewrite (leq_ltn_trans K F). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)