diff --git a/src/Init/Data/Range/Polymorphic.lean b/src/Init/Data/Range/Polymorphic.lean
index 2b9352bb87..c90630d9e9 100644
--- a/src/Init/Data/Range/Polymorphic.lean
+++ b/src/Init/Data/Range/Polymorphic.lean
@@ -11,6 +11,7 @@ public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Stream
 public import Init.Data.Range.Polymorphic.Lemmas
 public import Init.Data.Range.Polymorphic.Nat
+public import Init.Data.Range.Polymorphic.Int
 public import Init.Data.Range.Polymorphic.NatLemmas
 public import Init.Data.Range.Polymorphic.GetElemTactic
 
diff --git a/src/Init/Data/Range/Polymorphic/Int.lean b/src/Init/Data/Range/Polymorphic/Int.lean
new file mode 100644
index 0000000000..849e1418f4
--- /dev/null
+++ b/src/Init/Data/Range/Polymorphic/Int.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Order.Classes
+import Init.Omega
+
+public section
+
+namespace Std.PRange
+
+instance : UpwardEnumerable Int where
+  succ? x := some (x + 1)
+  succMany? n x := some (x + n)
+
+instance : LawfulUpwardEnumerable Int where
+  ne_of_lt := by
+    simp only [UpwardEnumerable.LT, UpwardEnumerable.succMany?, Option.some.injEq]
+    omega
+  succMany?_zero := by simp [UpwardEnumerable.succMany?]
+  succMany?_succ := by
+    simp only [UpwardEnumerable.succMany?, UpwardEnumerable.succ?,
+      Option.bind_some, Option.some.injEq]
+    omega
+
+instance : InfinitelyUpwardEnumerable Int where
+  isSome_succ? x := by simp [UpwardEnumerable.succ?]
+
+instance : LawfulUpwardEnumerableLE Int where
+  le_iff x y := by
+    simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, Int.le_def, Int.nonneg_def,
+      Int.sub_eq_iff_eq_add', eq_comm (a := y)]
+
+instance : RangeSize .closed Int where
+  size bound a := (bound + 1 - a).toNat
+
+instance : RangeSize .open Int := RangeSize.openOfClosed
+
+instance : LawfulRangeSize .closed Int where
+  size_eq_zero_of_not_isSatisfied bound x := by
+    simp only [SupportsUpperBound.IsSatisfied, RangeSize.size]
+    omega
+  size_eq_one_of_succ?_eq_none bound x := by
+    simp [SupportsUpperBound.IsSatisfied, RangeSize.size, UpwardEnumerable.succ?]
+
+  size_eq_succ_of_succ?_eq_some bound init x := by
+    simp only [SupportsUpperBound.IsSatisfied, UpwardEnumerable.succ?, RangeSize.size,
+      Option.some.injEq]
+    omega
+
+end Std.PRange
diff --git a/src/Init/Data/Range/Polymorphic/Nat.lean b/src/Init/Data/Range/Polymorphic/Nat.lean
index 33c72fcf86..d35993532d 100644
--- a/src/Init/Data/Range/Polymorphic/Nat.lean
+++ b/src/Init/Data/Range/Polymorphic/Nat.lean
@@ -15,9 +15,6 @@ import Init.Data.Order.Lemmas
 public section
 
 namespace Std.PRange
-open Std
-
--- induce LawfulUpwardEnumerable from antisymmetry and transitivity?
 
 instance : UpwardEnumerable Nat where
   succ? n := some (n + 1)
diff --git a/tests/lean/run/rangePolymorphic.lean b/tests/lean/run/rangePolymorphic.lean
index b340243129..b1a7ea23d2 100644
--- a/tests/lean/run/rangePolymorphic.lean
+++ b/tests/lean/run/rangePolymorphic.lean
@@ -86,3 +86,13 @@ i=4, j=6
 -/
 #guard_msgs in
 #eval h 5
+
+section Int
+
+example : ((-2)...3).toList = [-2, -1, 0, 1, 2] := by native_decide
+example : ((-2)...=3).toList = [-2, -1, 0, 1, 2, 3] := by native_decide
+
+example : Std.PRange.LawfulRangeSize .closed Int := inferInstance
+example : Std.PRange.LawfulRangeSize .open Int := inferInstance
+
+end Int