proposition: Lemma lastkey_mono A B (h1 : natmap A) (h2 : natmap B) : {subset dom h1 <= dom h2} -> last_key h1 <= last_key h2.
proof: Proof. rewrite leq_eqVlt orbC; apply: (seq_last_monoR _ (@otrans nat_ordType))=>//; by apply: hist_path. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)