proposition: Lemma lastkey_umfilt_dom A (h : natmap A) t : last_key (um_filterk (leq^~ t) h) <= last_key h.
proof: Proof. by apply: lastkey_mono; apply: dom_umfilt_subset. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)