From 1503fb75bc2f808ca73dc671e8fe2c1c923a98da Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Dec 2021 17:02:07 +0100
Subject: [PATCH] swap direction of mono_nat_lb_op

---
 iris/algebra/lib/mono_nat.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index defd93831..461382f81 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -45,7 +45,7 @@ Section mono_nat.
   Proof. by rewrite -mono_nat_auth_dfrac_op dfrac_op_own. Qed.
 
   Lemma mono_nat_lb_op n1 n2 :
-    â—¯MN n1 â‹… â—¯MN n2 = â—¯MN (n1 `max` n2).
+    â—¯MN (n1 `max` n2) = â—¯MN n1 â‹… â—¯MN n2.
   Proof. rewrite -auth_frag_op max_nat_op //. Qed.
 
   Lemma mono_nat_auth_lb_op dq n :
@@ -61,7 +61,7 @@ Section mono_nat.
   Lemma mono_nat_lb_op_le_l n n' :
     n' ≤ n →
     â—¯MN n = â—¯MN n' â‹… â—¯MN n.
-  Proof. intros. rewrite mono_nat_lb_op Nat.max_r //. Qed.
+  Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
 
   Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
   Proof.
-- 
GitLab