proposition: Lemma fresh_umfilt V (p : pred (nat * V)) (h : natmap V) : fresh (um_filter p h) <= fresh h.
proof: Proof. by apply: lastkey_umfilt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)