diff --git a/src/Init/Data/Range/Polymorphic.lean b/src/Init/Data/Range/Polymorphic.lean
index f6bfd45170..4893f752d9 100644
--- a/src/Init/Data/Range/Polymorphic.lean
+++ b/src/Init/Data/Range/Polymorphic.lean
@@ -18,6 +18,7 @@ public import Init.Data.Range.Polymorphic.UInt
 public import Init.Data.Range.Polymorphic.SInt
 
 public import Init.Data.Range.Polymorphic.NatLemmas
+public import Init.Data.Range.Polymorphic.IntLemmas
 public import Init.Data.Range.Polymorphic.GetElemTactic
 
 public section
diff --git a/src/Init/Data/Range/Polymorphic/IntLemmas.lean b/src/Init/Data/Range/Polymorphic/IntLemmas.lean
new file mode 100644
index 0000000000..047982cbb9
--- /dev/null
+++ b/src/Init/Data/Range/Polymorphic/IntLemmas.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Bentkamp
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Int
+public import Init.Data.Range.Polymorphic.Lemmas
+
+public section
+
+namespace Std.PRange.Int
+
+@[simp]
+theorem size_rco {a b : Int} :
+    (a...b).size = (b - a).toNat := by
+  simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size]
+  omega
+
+@[simp]
+theorem size_rcc {a b : Int} :
+    (a...=b).size = (b + 1 - a).toNat := by
+  simp [Rcc.size, Rxc.HasSize.size]
+
+@[simp]
+theorem size_roc {a b : Int} :
+    (a<...=b).size = (b - a).toNat := by
+  simp only [Roc.size, Rxc.HasSize.size]
+  omega
+
+@[simp]
+theorem size_roo {a b : Int} :
+    (a<...b).size = (b - a - 1).toNat := by
+  simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size]
+  omega
+
+end Std.PRange.Int