proposition: Lemma lastkey_subdom A1 A2 (h1 : natmap A1) (h2 : natmap A2) : {subset dom h1 <= dom h2} -> last_key h2 \in dom h1 -> last_key h1 = last_key h2.
proof: Proof. by move=>S D; apply/eqP; rewrite eqn_leq (lastkey_max D) (lastkey_mono S). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)