Remove redundant lemma

marcusrossel · marcusrossel · commit b4964e0179ce · 2025-06-09T16:41:33.000+02:00
diff --git a/HumanEvalLean/HumanEval155.lean b/HumanEvalLean/HumanEval155.lean
@@ -41,10 +41,6 @@ theorem digits_append_digits (hn : 0 < n) (hd : d < 10) :
 
 end Nat
 
-@[simp]
-theorem Int.digits_natAbs_cast (n : Nat) : (n : Int).natAbs.digits = n.digits := by
-  simp [Nat.digits]
-
 structure Tally where
   even : Nat
   odd  : Nat
