proposition: Lemma lastkeyF h : last_key h \in dom h -> last_key (free h (last_key h)) < last_key h.
proof: Proof. move=>D; case: (um_eta D)=>v [Ef] Eh. have N : last_key h \notin dom (free h (last_key h)). - by rewrite domF inE eqxx. have: last_key (free h (last_key h)) <= last_key h. - by apply: lastkey_mono=>x; rewrite domF inE; case: ifP. rewrite leq_eqVlt; case/orP=>// /eqP E; rewrite -{1}E in N. have Dn : last_key h > 0 by move/dom_cond: D; case: (last_key h). by rewrite -E in Dn; rewrite (dom_lastkeyE Dn) in N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)