diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 0087a71f171e16da43be66eef1def7b32f147ef3..046a7beb31fb6e0f325ee0a518e0486f0564fb12 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -560,8 +560,8 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
   match op, v2 with
   | OffsetOp, LitInt off => Some $ LitLoc (l1 +â‚— off)
-  | LeOp, LitLoc l2 => Some $ LitBool (bool_decide (loc_car l1 ≤ loc_car l2)%Z)
-  | LtOp, LitLoc l2 => Some $ LitBool (bool_decide (loc_car l1 < loc_car l2)%Z)
+  | LeOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 ≤ₗ l2))
+  | LtOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 <â‚— l2))
   | _, _ => None
   end.
 
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index 631e1be25d7a105c69312bd19b2401bc10c2b93a..124b0c16ded59d36b96ad29e4a4e39dadaf131ea 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -27,9 +27,17 @@ Module Loc.
   Definition add (l : loc) (off : Z) : loc :=
     {| loc_car := loc_car l + off|}.
 
+  Definition le (l1 l2 : loc) : Prop :=
+    loc_car l1 ≤ loc_car l2.
+
+  Definition lt (l1 l2 : loc) : Prop :=
+    loc_car l1 < loc_car l2.
+
   Module Import notations.
     Notation "l +â‚— off" :=
       (add l off) (at level 50, left associativity) : stdpp_scope.
+    Notation "l1 ≤ₗ l2" := (le l1 l2) (at level 70) : stdpp_scope.
+    Notation "l1 <â‚— l2" := (lt l1 l2) (at level 70) : stdpp_scope.
   End notations.
 
   Lemma add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
@@ -41,6 +49,44 @@ Module Loc.
   Global Instance add_inj l : Inj eq eq (add l).
   Proof. intros x1 x2. rewrite eq_spec /=. lia. Qed.
 
+  Global Instance le_dec l1 l2 : Decision (l1 ≤ₗ l2).
+  Proof. rewrite /le. apply _. Qed.
+
+  Global Instance lt_dec l1 l2 : Decision (l1 <â‚— l2).
+  Proof. rewrite /lt. apply _. Qed.
+
+  Global Instance le_po : PartialOrder le.
+  Proof.
+    rewrite /le. split; [split|].
+    - intros ?. reflexivity.
+    - intros ? ? ?. apply PreOrder_Transitive.
+    - intros [x] [y]. simpl. intros xy yx.
+      assert (x = y) by lia. congruence.
+  Qed.
+
+  Global Instance le_total : Total le.
+  Proof.
+    rewrite /le. intros ? ?.
+    apply Z.le_total.
+  Qed.
+
+  Lemma le_ngt l1 l2 : l1 ≤ₗ l2 ↔ ¬l2 <ₗ l1.
+  Proof.
+    rewrite /le /lt. intuition lia.
+  Qed.
+
+  Lemma le_lteq l1 l2 : l1 ≤ₗ l2 ↔ l1 <ₗ l2 ∨ l1 = l2.
+  Proof.
+    rewrite /le /lt. destruct l1 as [x], l2 as [y]. simpl.
+    intuition.
+    - assert (x < y ∨ x = y)%Z by lia. intuition congruence.
+    - lia.
+    - assert (x = y) by congruence. lia.
+  Qed.
+
+  Lemma add_le l1 l2 i1 i2 : l1 ≤ₗ l2 → (i1 ≤ i2)%Z → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
+  Proof. rewrite /le /add. simpl. lia. Qed.
+
   Definition fresh (ls : gset loc) : loc :=
     {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.