diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index e6ea1b9e37af08ef4f474c5d1742b07ca9bef4d3..98c53efb08e04f302e5ccdecb648dc6ad90e3ea4 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 //; [].