proposition: Lemma lastkey_leq A (h : natmap A) x : {in dom h, forall y, y <= x} <-> last_key h <= x.
proof: Proof. split; last by move=>D y Y; apply: leq_trans D; apply: lastkey_max Y. case V : (valid h); last first. - by move/negbT/invalidE: V=>->; rewrite lastkey_undef. case E: (unitb h); first by move/unitbP: E=>->; rewrite lastkey0. by apply; rewrite dom_lastkey // E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)