proposition: Lemma omg_lastkey x y : (omg x = own -> valid (x \+ y) -> omg_s x y -> last_key (x \+ y) = last_key x) * (omg y = own -> valid (x \+ y) -> omg_s x y -> last_key (x \+ y) = last_key y).
proof: Proof. rewrite /omg_s /omg; split=>L V S; case: ifP L=>L // _; rewrite L /= in S; rewrite lastkeyUn V; case/andP: S=>S1 S2. by rewrite maxnC /maxn S1. by rewrite /maxn S2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)