proposition: Lemma umfilt_le_last A (h : natmap A) t : last_key h <= t -> um_filter (le t) h = h.
proof: Proof. case V : (valid h); last first. - by move/invalidE: (negbT V)=>->; rewrite umfilt_undef. move=>N; rewrite -{2}[h]umfilt_predT; apply/eq_in_umfilt. by case=>k v /In_dom/lastkey_max/leq_trans; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)