From ae9d12aeaa075578c7ee3a5a585d0f9fb89cedd2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Thu, 13 Feb 2025 14:19:02 +1100
Subject: [PATCH] chore: upstream an Int lemma (#7060)

---
 src/Init/Data/Int/Lemmas.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index 6231d0dc6f..42d8d86e75 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -326,6 +326,10 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
   · exact (Nat.add_sub_cancel_left ..).symm
   · dsimp; rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]; rfl
 
+theorem toNat_of_nonpos : ∀ {z : Int}, z ≤ 0 → z.toNat = 0
+  | 0, _ => rfl
+  | -[_+1], _ => rfl
+
 /- ## add/sub injectivity -/
 
 protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by