proposition: Lemma lastkey_omap_some V1 V2 (f : nat * V1 -> option V2) (h : natmap V1) : (forall x, x \In h -> oapp predT false (f x)) -> last_key (omap f h) = last_key h.
proof: Proof. by rewrite /last_key=>/dom_omap_some ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)