feat: add lemmas about Int range sizes (#11159)

This PR adds lemmas about the sizes of ranges of Ints, analogous to the
Nat lemmas in `Init.Data.Range.Polymorphic.NatLemmas`. See also
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Reasonning.20about.20PRange.20sizes.20.28with.20.60Int.60.29/with/546466339.

Closes #11158

---------

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

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

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