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