diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index ac67d09f126951794282d3ec639ebf015bd4d69f..631e1be25d7a105c69312bd19b2401bc10c2b93a 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -44,8 +44,7 @@ Module Loc.
   Definition fresh (ls : gset loc) : loc :=
     {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.
 
-  Lemma fresh_fresh ls i :
-    (0 ≤ i)%Z → fresh ls +ₗ i ∉ ls.
+  Lemma fresh_fresh ls i : 0 ≤ i → fresh ls +ₗ i ∉ ls.
   Proof.
     intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh ls) + i).
     { intros help Hf%help. simpl in *. lia. }