proposition: Lemma lastkey_omap V1 V2 (f : nat * V1 -> option V2) (h : natmap V1) : last_key (omap f h) <= last_key h.
proof: Proof. by apply: lastkey_mono; apply: dom_omap_sub. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)