chore: remove Int simp lemmas that can't fire (#5253)

```
#lint only simpNF in all
```
reports (amongst others):

```
-- Init.Data.Int.Order
#check @Int.toNat_of_nonneg /- Left-hand side simplifies from
  ↑a.toNat
to
  max a 0
using
  simp only [Int.ofNat_toNat]
Try to change the left-hand side to the simplified term!
 -/
#check Int.toNat_sub_toNat_neg /- Left-hand side simplifies from
  ↑n.toNat - ↑(-n).toNat
to
  max n 0 - max (-n) 0
using
  simp only [Int.ofNat_toNat]
Try to change the left-hand side to the simplified term!
 -/
```

src/Init/Data/Int/Order.lean

@@ -480,7 +480,7 @@ theorem toNat_eq_max : ∀ a : Int, (toNat a : Int) = max a 0
 
 @[simp] theorem toNat_one : (1 : Int).toNat = 1 := rfl
 
-@[simp] theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
+theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
   rw [toNat_eq_max, Int.max_eq_left h]
 
 @[simp] theorem toNat_ofNat (n : Nat) : toNat ↑n = n := rfl
@@ -515,7 +515,7 @@ theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toN
   | (n+1:Nat) => by simp [ofNat_add]
   | -[n+1] => rfl
 
-@[simp] theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
+theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
   | 0 => rfl
   | (_+1:Nat) => Int.sub_zero _
   | -[_+1] => Int.zero_sub _