leanprover · TwoFX · Apr 25, 2025 · Apr 22, 2025 · Apr 22, 2025 · Apr 25, 2025
@@ -1358,7 +1358,7 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) :
   rcases w with _|w
   · simp [toInt_of_zero_length, Int.min_eq_right]
   · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this]
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod, Int.neg_inj]
     rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])]
 
 /--
@@ -1574,7 +1574,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
 
 theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) :
     x.toInt = -((-x).toNat) := by
-  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
+  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.natCast_emod]
   norm_cast
   rw [Nat.mod_eq_of_lt]
   · omega
@@ -1669,7 +1669,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           (a.sdiv b).toInt = -((-a).toNat / b.toNat) := by
         simp only [sdiv_eq, ha, hb, udiv_eq]
         rw [toInt_eq_neg_toNat_neg_of_nonpos]
-        · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
+        · rw [neg_neg, toNat_udiv, toNat_neg, Int.natCast_emod, Int.neg_inj]
           norm_cast
         · rw [neg_eq_zero_iff]
           by_cases h' : -a / b = 0#w

@@ -620,10 +620,10 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
   simp only [toInt_eq_toNat_cond]
   split
   next g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
+    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
   next g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
+    rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
 
 theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by
@@ -639,7 +639,7 @@ theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.t
 @[simp] theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by
   rw [toInt_eq_msb_cond]
   simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte,
-    toNat_ofNat, Int.ofNat_emod]
+    toNat_ofNat, Int.natCast_emod]
   norm_cast
   apply Nat.mod_eq_of_lt
   apply Nat.one_lt_two_pow (by omega)
@@ -2548,7 +2548,7 @@ where
       simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
       omega
     have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega)
-    simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
+    simp only [this, toNat_setWidth, Int.natCast_add, Int.natCast_emod, Int.natCast_mul]
     by_cases h : x.msb
     <;> norm_cast
     <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow]
@@ -3871,7 +3871,7 @@ theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by
 theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w := by
   constructor
   · intro h₂
-    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_emod, Int.ofNat_one, Int.natCast_pow,
+    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.natCast_emod, Int.ofNat_one, Int.natCast_pow,
       Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂
     simp [toNat_eq, show x.toNat = 0 by omega]
   · simp_all
@@ -5056,7 +5056,7 @@ theorem toInt_intMin_le (x : BitVec w) :
   cases w
   case zero => simp [toInt_intMin, @of_length_zero x]
   case succ w =>
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod]
     have : 0 < 2 ^ w := Nat.two_pow_pos w
     rw [Int.emod_eq_of_lt (by omega) (by omega)]
     rw [BitVec.toInt_eq_toNat_bmod]

@@ -94,7 +94,7 @@ def resolve_left' (a c d p x : Int) (h₁ : p ≤ a * x) : Nat := (add_of_le h
 
 @[simp] theorem resolve_left_eq (a c d p x : Int) (h₁ : p ≤ a * x) :
     resolve_left a c d p x = resolve_left' a c d p x h₁ := by
-  simp only [resolve_left, resolve_left', add_of_le, ofNat_emod, ofNat_toNat]
+  simp only [resolve_left, resolve_left', add_of_le, natCast_emod, ofNat_toNat]
   rw [Int.max_eq_left]
   omega
 
@@ -129,14 +129,14 @@ theorem resolve_left_dvd₁ (a c d p x : Int) (h₁ : p ≤ a * x) :
     a ∣ resolve_left a c d p x + p := by
   simp only [h₁, resolve_left_eq, resolve_left']
   obtain ⟨k', w⟩ := add_of_le h₁
-  exact Int.ofNat_emod _ _ ▸ dvd_emod_add_of_dvd_add (x := k') ⟨x, by rw [w, Int.add_comm]⟩ (dvd_lcm_left ..)
+  exact Int.natCast_emod _ _ ▸ dvd_emod_add_of_dvd_add (x := k') ⟨x, by rw [w, Int.add_comm]⟩ (dvd_lcm_left ..)
 
 theorem resolve_left_dvd₂ (a c d p x : Int)
     (h₁ : p ≤ a * x) (h₃ : d ∣ c * x + s) :
     a * d ∣ c * resolve_left a c d p x + c * p + a * s := by
   simp only [h₁, resolve_left_eq, resolve_left']
   obtain ⟨k', w⟩ := add_of_le h₁
  simp only [Int.add_assoc, ofNat_emod]
+  simp only [Int.add_assoc, natCast_emod]
   apply dvd_mul_emod_add_of_dvd_mul_add
   · obtain ⟨z, r⟩ := h₃
     refine ⟨z, ?_⟩

@@ -112,7 +112,10 @@ because mathematical reasoning tends to be easier.
 instance : Mod Int where
   mod := Int.emod
 
-@[norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+@[simp, norm_cast] theorem natCast_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+
+@[deprecated natCast_ediv (since := "2025-04-17")]
+theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := natCast_ediv m n
 
 theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
 @[norm_cast]

@@ -34,7 +34,7 @@ protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])
 
 @[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
-  refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
+  refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.natCast_mul]⟩⟩
   match Int.le_total a 0 with
   | .inl h =>
     have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
@@ -89,7 +89,10 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
 
 /-! ### ofNat mod -/
 
-@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
+@[simp, norm_cast] theorem natCast_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
+
+@[deprecated natCast_emod (since := "2025-04-17")]
+theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := natCast_emod m n
 
 /-! ### mod definitions -/
 
@@ -103,7 +106,7 @@ theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
   | -[m+1], -[n+1] => aux m n.succ
 where
   aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1] := by
-    rw [← ofNat_emod, ← ofNat_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n,
+    rw [← natCast_emod, ← natCast_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n,
       ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
     exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
 
@@ -184,7 +187,7 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a
   rw [Int.div_def]
   match b, h with
   | Int.ofNat (b+1), _ =>
-    rcases a with ⟨a⟩ <;> simp [Int.ediv]
+    rcases a with ⟨a⟩ <;> simp [Int.ediv, -natCast_ediv]
 
 @[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
 abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos

@@ -604,8 +604,6 @@ theorem sign_ediv (a b : Int) : sign (a / b) = if 0 ≤ a ∧ a < b.natAbs then
       | negSucc a =>
         norm_cast
 
-@[simp, norm_cast] theorem natCast_ediv (m n : Nat) : ((m / n : Nat) : Int) = m / n := rfl
-
 /-! ### emod -/
 
 theorem mod_def' (m n : Int) : m % n = emod m n := rfl
@@ -714,8 +712,6 @@ theorem one_emod {b : Int} : 1 % b = if b.natAbs = 1 then 0 else 1 := by
 
 @[simp] theorem neg_emod_two (i : Int) : -i % 2 = i % 2 := by omega
 
-@[simp, norm_cast] theorem natCast_emod (m n : Nat) : (↑(m % n) : Int) = ↑m % ↑n := rfl
-
 /-! ### properties of `/` and `%` -/
 
 theorem mul_ediv_cancel_of_dvd {a b : Int} (H : b ∣ a) : b * (a / b) = a :=
@@ -1325,7 +1321,7 @@ theorem lt_tmod_of_pos (a : Int) {b : Int} (H : 0 < b) : -b < tmod a b :=
   match a, b, eq_succ_of_zero_lt H with
   | ofNat _, _, ⟨n, rfl⟩ => by rw [ofNat_eq_coe, ← Int.natCast_succ, ← ofNat_tmod]; omega
   | -[a+1], _, ⟨n, rfl⟩ => by
-    rw [negSucc_eq, neg_tmod, ← Int.natCast_succ, ← Int.natCast_succ, ← ofNat_tmod]
+    rw [negSucc_eq, neg_tmod, ← Int.natCast_add_one, ← Int.natCast_add_one, ← ofNat_tmod]
     have : (a + 1) % (n + 1) < n + 1 := Nat.mod_lt _ (Nat.zero_lt_succ n)
     omega
 
@@ -2017,7 +2013,7 @@ theorem neg_fdiv {a b : Int} : (-a).fdiv b = -(a.fdiv b) - if b = 0 ∨ b ∣ a
     rw [neg_negSucc, ← negSucc_eq]
   | -[a+1], -[b+1] =>
     unfold fdiv
-    simp only [ofNat_eq_coe, ofNat_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int]
+    simp only [ofNat_eq_coe, natCast_ediv, Nat.succ_eq_add_one, Int.natCast_add, cast_ofNat_Int]
     rw [neg_negSucc, neg_negSucc]
     simp
 
@@ -2903,7 +2899,7 @@ theorem ediv_lt_self_of_pos_of_ne_one {x y : Int} (hx : 0 < x) (hy : y ≠ 1) :
   by_cases hy' : 1 < y
   · obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
     obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega)
-    rw [← Int.ofNat_ediv]
+    rw [← Int.natCast_ediv]
     norm_cast
     apply Nat.div_lt_self (by omega) (by omega)
   · have := @Int.ediv_nonpos_of_nonneg_of_nonpos x y (by omega) (by omega)
@@ -2913,7 +2909,7 @@ theorem ediv_nonneg_of_nonneg_of_nonneg {x y : Int} (hx : 0 ≤ x) (hy : 0 ≤ y
     0 ≤ x / y := by
   obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
   obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega)
-  rw [← Int.ofNat_ediv]
+  rw [← Int.natCast_ediv]
   exact Int.ofNat_zero_le (xn / yn)
 
 /--  When both x and y are negative we need stricter bounds on x and y

@@ -25,9 +25,17 @@ theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat
 
 @[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl
 
-@[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
-@[norm_cast] theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
-@[norm_cast] theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
+@[simp, norm_cast] theorem natCast_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
+@[simp, norm_cast] theorem natCast_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
+@[norm_cast] theorem natCast_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
+@[norm_cast] theorem natCast_add_one (n : Nat) : ((n + 1 : Nat) : Int) = n + 1 := rfl
+
+@[deprecated natCast_add (since := "2025-04-17")]
+theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
+@[deprecated natCast_mul (since := "2025-04-17")]
+theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
+@[deprecated natCast_succ (since := "2025-04-17")]
+theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
 
 theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
 theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
@@ -157,7 +165,7 @@ theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k :=
     conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
     apply subNatNat_add_add
   | inr h' => simp [subNatNat_of_le h',
-      subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']
+      subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h', -natCast_add]
 
 theorem subNatNat_add_negSucc (m n k : Nat) :
     subNatNat m n + -[k+1] = subNatNat m (n + succ k) := by
@@ -184,7 +192,7 @@ theorem subNatNat_self : ∀ n, subNatNat n n = 0
 /- addition -/
 
 protected theorem add_comm : ∀ a b : Int, a + b = b + a
-  | ofNat n, ofNat m => by simp [Nat.add_comm]
+  | ofNat n, ofNat m => by simp [Nat.add_comm, -natCast_add]
   | ofNat _, -[_+1]  => rfl
   | -[_+1],  ofNat _ => rfl
   | -[_+1],  -[_+1]  => by simp [Nat.add_comm]
@@ -218,8 +226,8 @@ protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
     simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
 where
   aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c)
-    | (k:Nat) => by simp [Nat.add_assoc]
-    | -[k+1]  => by simp [subNatNat_add]
+    | (k:Nat) => by simp [Nat.add_assoc, -natCast_add]
+    | -[k+1]  => by simp [subNatNat_add, -natCast_add]
   aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
     simp
     rw [Int.add_comm, subNatNat_add_negSucc]
@@ -236,8 +244,8 @@ protected theorem add_right_comm (a b c : Int) : a + b + c = a + c + b := by
 
 protected theorem add_left_neg : ∀ a : Int, -a + a = 0
   | 0      => rfl
-  | succ m => by simp [neg_ofNat_succ]
-  | -[m+1] => by simp [neg_negSucc]
+  | succ m => by simp [neg_ofNat_succ, -natCast_add]
+  | -[m+1] => by simp [neg_negSucc, -natCast_add]
 
 protected theorem add_right_neg (a : Int) : a + -a = 0 := by
   rw [Int.add_comm, Int.add_left_neg]
@@ -283,7 +291,7 @@ theorem wlog_sign {P : Int → Prop} (inv : ∀ i, P i ↔ P (-i)) (w : ∀ n :
   cases i with
   | ofNat n => exact w n
   | negSucc n =>
-    rw [negSucc_eq, ← inv, ← ofNat_succ]
+    rw [negSucc_eq, ← inv, ← natCast_succ]
     apply w
 
 /- ## subtraction -/
@@ -342,10 +350,10 @@ theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by
 protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by
   apply subNatNat_elim m n fun m n i => i = m - n
   · intros i n
-    rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
+    rw [Int.natCast_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
       Int.add_right_neg, Int.add_zero]
   · intros i n
-    simp only [negSucc_eq, ofNat_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
+    simp only [negSucc_eq, natCast_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
     rw [Int.add_neg_eq_sub (a := n), ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
     apply Nat.le_refl
 
@@ -410,7 +418,7 @@ theorem negSucc_mul_ofNat (m n : Nat) : -[m+1] * n = -↑(succ m * n) := rfl
 theorem negSucc_mul_negSucc (m n : Nat) : -[m+1] * -[n+1] = succ m * succ n := rfl
 
 protected theorem mul_comm (a b : Int) : a * b = b * a := by
-  cases a <;> cases b <;> simp [Nat.mul_comm]
+  cases a <;> cases b <;> simp [Nat.mul_comm, -natCast_mul]
 instance : Std.Commutative (α := Int) (· * ·) := ⟨Int.mul_comm⟩
 
 theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
@@ -427,7 +435,8 @@ theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ
 
 protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
   cases a <;> cases b <;> cases c <;>
-    simp [Nat.mul_assoc, ofNat_mul_negOfNat, negOfNat_mul_ofNat, negSucc_mul_negOfNat, negOfNat_mul_negSucc]
+    simp [Nat.mul_assoc, ofNat_mul_negOfNat, negOfNat_mul_ofNat, negSucc_mul_negOfNat,
+      negOfNat_mul_negSucc, -natCast_mul]
 
 instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩
 
@@ -450,12 +459,14 @@ theorem ofNat_mul_subNatNat (m n k : Nat) :
   | succ m => cases n.lt_or_ge k with
     | inl h =>
       have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
-      simp [subNatNat_of_lt h, subNatNat_of_lt h']
+      simp only [subNatNat_of_lt h, pred_eq_sub_one, ofNat_mul_negSucc', succ_eq_add_one,
+        subNatNat_of_lt h']
       rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
         ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
     | inr h =>
       have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
-      simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]
+      simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib,
+        -natCast_mul, -natCast_add]
 
 theorem negOfNat_add (m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n) := by
   cases m <;> cases n <;> simp [Nat.succ_add] <;> rfl
@@ -476,17 +487,17 @@ theorem negSucc_mul_subNatNat (m n k : Nat) :
 
 attribute [local simp] ofNat_mul_subNatNat negOfNat_add negSucc_mul_subNatNat in
 protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
-  | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib]
+  | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib, -natCast_add, -natCast_mul]
   | (m:Nat), (n:Nat), -[k+1]  => by
-    simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
+    simp [negOfNat_eq_subNatNat_zero, -natCast_mul]; rw [← subNatNat_add]; rfl
   | (m:Nat), -[n+1],  (k:Nat) => by
-    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
+    simp [negOfNat_eq_subNatNat_zero, -natCast_mul]; rw [Int.add_comm, ← subNatNat_add]; rfl
   | (m:Nat), -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
-  | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm]
+  | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm, -natCast_mul, -natCast_add]; rw [← Nat.right_distrib, Nat.mul_comm]
   | -[m+1],  (n:Nat), -[k+1]  => by
-    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
-  | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
-  | -[m+1],  -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
+    simp [negOfNat_eq_subNatNat_zero, -natCast_add, -natCast_mul]; rw [Int.add_comm, ← subNatNat_add]; rfl
+  | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero, -natCast_add, -natCast_mul]; rw [← subNatNat_add]; rfl
+  | -[m+1],  -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc, -natCast_mul]
 
 protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
   simp [Int.mul_comm, Int.mul_add]
@@ -583,12 +594,4 @@ protected theorem natCast_zero : ((0 : Nat) : Int) = (0 : Int) := rfl
 
 protected theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
 
-@[simp, norm_cast] protected theorem natCast_add (a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int) := by
-  rfl
-
-protected theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : Int) = (n : Int) + 1 := rfl
-
-@[simp] protected theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
-  simp
-
 end Int
@@ -48,7 +48,7 @@ def Expr.denoteAsInt (ctx : Context) : Expr → Int
   | .mod a b  => Int.emod (denoteAsInt ctx a) (denoteAsInt ctx b)
 
 theorem Expr.denoteAsInt_eq (ctx : Context) (e : Expr) : e.denoteAsInt ctx = e.denote ctx := by
-  induction e <;> simp [denote, denoteAsInt, Int.ofNat_ediv, *] <;> rfl
+  induction e <;> simp [denote, denoteAsInt, Int.natCast_ediv, *] <;> rfl
 
 theorem Expr.eq_denoteAsInt (ctx : Context) (e : Expr) : e.denote ctx = e.denoteAsInt ctx := by
   apply Eq.symm; apply denoteAsInt_eq