use < and <= instead of > and >=

1da42076 · Ralf Jung · e4b58ebf · 1da42076
Commit 1da42076 authored Feb 11, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 2 deletions

heap_lang/sugar.v heap_lang/sugar.v +2 -2

No files found.
--- 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 //; [].