proposition: Lemma lastkey_umfilt_leq A (h : natmap A) t : last_key (um_filterk (leq^~ t) h) <= t.
proof: Proof. case V : (valid h); last first. - by move/negbT/invalidE: V=>->; rewrite umfilt_undef lastkey_undef. have V' : valid (um_filterk (leq^~ t) h) by rewrite valid_umfilt. case E : (unitb (um_filterk (leq^~ t) h)). - by move/unitbP: E=>->; rewrite lastkey0. by case/dom_umfilt: (dom_lastkey V' (negbT E))=>v []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)