proposition: Lemma lastatval_indomb h : last_atval false h -> last_key h \in dom h.
proof: Proof. by move=>H; apply: (lastatval_indom (v:=false)); rewrite H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)