From 13117f43b4b7b8e733ec6e17ab2b29ffb984e4c9 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 1 Jul 2016 20:38:24 +0200
Subject: [PATCH] Local update for nat

---
 algebra/updates.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/algebra/updates.v b/algebra/updates.v
index 040f563c4..9338c0762 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -239,3 +239,13 @@ Section option.
   Lemma option_update x y : x ~~> y → Some x ~~> Some y.
   Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
 End option.
+
+(** * Natural numbers  *)
+Lemma nat_local_update (x y : nat) mz :
+  x ~l~> y @ mz.
+Proof.
+  split. done.
+  unfold opM, op, dist, cofe_dist, cmra_cofeC, cmra_op, cmra_dist, natR, nat_op,
+         discrete_dist, equiv, equivL.
+  destruct mz as [z|]; intros n [z'|]; lia.
+Qed.
-- 
GitLab