From 124e34ef5abdeb29ca20ba9ee602568f7c789ff8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 11 Dec 2025 10:10:26 +1100
Subject: [PATCH] feat: `grind_pattern natCast_nonneg` (#11574)

This PR adds a lemma that the cast of a natural number into any ordered
ring is non-negative. We can't annotate this directly for `grind`, but
will probably add this to `grind`'s linarith interrnals.
---
 src/Init/Grind/Ordered/Ring.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean
index cd01ac6ca6..3bea9e8d09 100644
--- a/src/Init/Grind/Ordered/Ring.lean
+++ b/src/Init/Grind/Ordered/Ring.lean
@@ -151,6 +151,9 @@ theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) :
     simp [Semiring.natCast_add, Semiring.natCast_one]
     exact OrderedAdd.add_le_left_iff _ |>.mp ih
 
+theorem natCast_nonneg {a : Nat} : 0 ≤ (a : R) := by
+  simpa [Semiring.natCast_zero] using natCast_le_natCast_of_le (R := R) _ _ (Nat.zero_le a)
+
 theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b → (a : R) < (b : R) := by
   induction a generalizing b <;> cases b <;> simp
   next n =>