proposition: Lemma omg_eta (h : natmap (bool * bool)): valid h -> omg h = own -> exists h' v, [/\ h' = free h (last_key h), h = last_key h \-> (v, true) \+ h', last_key h != 0, last_key h \in dom h, last_key h \notin dom h' & last_key h' < last_key h].
proof: Proof. rewrite /omg; case: ifP=>// N V _; set k := last_key h. have D : k \in dom h. - rewrite /last_atval /atval /oapp in N. by case: dom_find N=>[->//|]. have K : k != 0 by apply: dom_cond D. case: (um_eta D); case=>v1 v2 [Ef Eh]. set h' := free h k in Eh *; set q := k \-> (v1, true). have Nd : k \notin dom h'. - rewrite Eh in V; case: validUn V=>// _ _ X _; apply: X. by rewrite domPt inE /= K eq_refl. exists h', v1; split=>//. - by rewrite /last_atval /atval Ef /= in N; rewrite -N. have: last_key h' <= k. - by rewrite /k Eh; apply: lastkeyUnf; rewrite -Eh. rewrite leq_eqVlt; case/orP=>// /eqP E. rewrite -E in Nd; apply: contraR Nd=>/= _. by apply: (dom_lastkeyE (a:=0)); rewrite E; case: (k) K. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)