proposition: Lemma omg_fresh_sep (V : pcm) (v1 v2 : V) (D : sep_rel V) (ht : @morphism V U D) op : valid (v1 \+ v2) -> D v1 v2 -> (omg (ht v2) = nown -> omg_s (fresh (ht v1 \+ ht v2) \-> op \+ ht v1) (ht v2)) * (omg (ht v1) = nown -> omg_s (ht v1) (fresh (ht v1 \+ ht v2) \-> op \+ ht v2)).
proof: Proof. move=>A O; have Vh : valid (ht v1 \+ ht v2). - by move/pfV2: O; move/(_ _ ht A). rewrite /omg_s lastatval_freshUn // lastkey_freshUn //. split=>N; first by rewrite omgP N /fresh lastkeyUn Vh ltnS leq_maxr implybT. by rewrite omgP N lastkey_freshUn //= ltnS lastkeyUn Vh leq_maxl implybT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)