From 1da42076e201b613f67fe1586ceb38785e9129ed Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 20:07:51 +0100
Subject: [PATCH] use < and <= instead of > and >=

---
 heap_lang/sugar.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index e6ea1b9e3..98c53efb0 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -80,7 +80,7 @@ Qed.
 
 Lemma wp_le E (n1 n2 : nat) P Q :
   (n1 â‰¤ n2 â†’ P âŠ‘ â–· Q (LitV true)) â†’
-  (n1 > n2 â†’ P âŠ‘ â–· Q (LitV false)) â†’
+  (n2 < n1 â†’ P âŠ‘ â–· Q (LitV false)) â†’
   P âŠ‘ wp E ('n1 â‰¤ 'n2) Q.
 Proof.
   intros. rewrite -wp_bin_op //; [].
@@ -89,7 +89,7 @@ Qed.
 
 Lemma wp_lt E (n1 n2 : nat) P Q :
   (n1 < n2 â†’ P âŠ‘ â–· Q (LitV true)) â†’
-  (n1 â‰¥ n2 â†’ P âŠ‘ â–· Q (LitV false)) â†’
+  (n2 â‰¤ n1 â†’ P âŠ‘ â–· Q (LitV false)) â†’
   P âŠ‘ wp E ('n1 < 'n2) Q.
 Proof.
   intros. rewrite -wp_bin_op //; [].
-- 
GitLab