chore: deprecate unused norm_cast lemma (leanprover-community#35604)

This lemma does not appear to fire as a norm_cast lemma and outside of norm_cast, Nat.cast_sub should be used instead.

Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>

Author: DavidLedvinka

Mathlib/Tactic/Zify.lean

@@ -116,7 +116,8 @@ def zifyProof (simpArgs : Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar
 
 variable {R : Type*} [AddGroupWithOne R]
 
-@[norm_cast] theorem Nat.cast_sub_of_add_le {m n k} (h : m + k ≤ n) :
+@[deprecated "use Nat.cast_sub" (since := "2026-02-21"), norm_cast]
+theorem Nat.cast_sub_of_add_le {m n k} (h : m + k ≤ n) :
     ((n - m : ℕ) : R) = n - m := Nat.cast_sub (m.le_add_right k |>.trans h)
 
 @[norm_cast] theorem Nat.cast_sub_of_lt {m n} (h : m < n) :