diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index d77e3cb6d5..f1f3c7455a 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1371,6 +1371,261 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
+@[simp]
+theorem ne_intMin_of_lt_of_msb_false {x : BitVec w} (hw : 0 < w) (hx : x.msb = false) :
+    x ≠ intMin w := by
+  have := toNat_lt_of_msb_false hx
+  simp [toNat_eq, Nat.two_pow_pred_mod_two_pow hw]
+  omega
+
+@[simp]
+theorem ne_zero_of_msb_true {x : BitVec w} (hx : x.msb = true) :
+    x ≠ 0#w := by
+  have := Nat.two_pow_pos (w-1)
+  have := le_toNat_of_msb_true hx
+  simp [toNat_eq]
+  omega
+
+@[simp]
+theorem msb_neg_of_ne_intMin_of_ne_zero {x : BitVec w} (h : x ≠ intMin w) (h' : x ≠ 0#w) :
+    (-x).msb = !x.msb := by
+  simp only [msb_neg, bool_to_prop]
+  simp [h, h']
+
+@[simp]
+theorem udiv_intMin_of_msb_false {x : BitVec w} (h : x.msb = false) :
+    x / intMin w = 0#w := by
+  by_cases hw : w = 0
+  · subst hw
+    decide +revert
+  have wpos : 0 < w := by omega
+  have := Nat.two_pow_pos (w-1)
+  simp [toNat_eq, wpos]
+  rw [Nat.div_eq_zero_iff_lt (by omega)]
+  exact toNat_lt_of_msb_false h
+
+theorem sdiv_intMin {x : BitVec w} :
+    x.sdiv (intMin w) = if x = intMin w then 1#w else 0#w := by
+  by_cases hw : w = 0
+  · subst hw
+    decide +revert
+  have wpos : 0 < w := by omega
+  by_cases h : x = intMin w
+  · subst h
+    simp
+    omega
+  · simp only [sdiv_eq, msb_intMin, show 0 < w by omega, h]
+    have := Nat.two_pow_pos (w-1)
+    by_cases hx : x.msb
+    · simp [msb_neg_of_ne_intMin_of_ne_zero (by simp [h])
+        (BitVec.ne_zero_of_msb_true hx), hx]
+    · simp [hx]
+
+theorem sdiv_neg {x y : BitVec w} (h : y ≠ intMin w) :
+    x.sdiv (-y) = -(x.sdiv y) := by
+  by_cases h' : y = 0#w
+  · subst h'
+    simp
+  · simp only [BitVec.sdiv, msb_neg_of_ne_intMin_of_ne_zero h (by simp [h'])]
+    cases x.msb <;> cases y.msb <;> simp
+
+theorem neg_sdiv {x y : BitVec w} (h : x ≠ intMin w) :
+    (-x).sdiv y = -(x.sdiv y) := by
+  by_cases hx0 : x = 0#w
+  · subst hx0
+    simp
+  · simp only [BitVec.sdiv, msb_neg_of_ne_intMin_of_ne_zero h (by simp [hx0])]
+    cases x.msb <;> cases y.msb <;> simp
+
+theorem neg_sdiv_neg {x y : BitVec w} (h : x ≠ intMin w) :
+    (-x).sdiv (-y) = x.sdiv y := by
+  by_cases h' : y = intMin w
+  · subst h'
+    simp [sdiv_intMin, neg_intMin]
+  · by_cases hy0 : y = 0#w
+    · subst hy0
+      simp
+    · by_cases hx0 : x = 0#w
+      · subst hx0
+        simp
+      · simp only [BitVec.sdiv,
+           msb_neg_of_ne_intMin_of_ne_zero h  (by simp [hx0]),
+           msb_neg_of_ne_intMin_of_ne_zero h' (by simp [hy0])]
+        cases x.msb <;> cases y.msb <;> simp
+
+theorem intMin_eq_neg_two_pow : intMin w = BitVec.ofInt w (-2 ^ (w - 1)) := by
+  apply BitVec.eq_of_toInt_eq
+  refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; simp [BitVec.toInt_zero_length]) (fun hw => ?_)
+  rw [BitVec.toInt_intMin_of_pos hw, BitVec.toInt_ofInt_eq_self hw (Int.le_refl _)]
+  have := Nat.two_pow_pos (w - 1)
+  norm_cast
+  omega
+
+theorem toInt_intMin_eq_bmod : (intMin w).toInt = (-2 ^ (w - 1)).bmod (2 ^ w) := by
+  rw [intMin_eq_neg_two_pow, toInt_ofInt]
+
+@[simp]
+theorem toInt_bmod_cancel(b : BitVec w) : b.toInt.bmod (2 ^ w) = b.toInt := by
+  rw [toInt_eq_toNat_bmod, Int.bmod_bmod]
+
+theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
+    x.sdiv y ≠ intMin w := by
+  by_cases hw : w = 0
+  · subst hw
+    simp [BitVec.eq_nil x] at h
+    contradiction
+  simp only [sdiv, udiv_eq, neg_eq]
+  by_cases hx : x.msb <;> by_cases hy : y.msb
+  <;> simp only [hx, hy, neg_ne_intMin_inj]
+  <;> simp only [Bool.not_eq_true] at hx hy
+  <;> apply ne_intMin_of_lt_of_msb_false (by omega)
+  <;> rw [msb_udiv]
+  <;> try simp only [hx, Bool.false_and]
+  · simp [h, ne_zero_of_msb_true, hx]
+  · simp [h, ne_zero_of_msb_true, hx]
+
+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]
+  norm_cast
+  rw [Nat.mod_eq_of_lt]
+  · omega
+  · have := @BitVec.isLt w x
+    have ne_zero := ne_zero_of_msb_true h
+    simp only [ne_eq, toNat_eq, toNat_ofNat, zero_mod] at ne_zero
+    omega
+
+theorem toInt_eq_neg_toNat_neg_of_nonpos {x : BitVec w} (h : x = 0#w ∨ x.msb = true) :
+    x.toInt = -((-x).toNat) := by
+  cases h
+  case inl h' =>
+    simp [h']
+  case inr h' =>
+    simp [toInt_eq_neg_toNat_neg_of_msb_true h']
+
+theorem intMin_udiv_eq_intMin_iff (x : BitVec w) :
+    intMin w / x = intMin w ↔ x = 1#w := by
+  by_cases hw : w = 0;   subst hw; decide +revert
+  by_cases hx : x = 1#w; subst hx; simp
+  have wpos : 0 < w := by omega
+
+  have : 0 ≤ (2 ^ (w - 1) / x.toNat) := by simp
+  have := Nat.two_pow_pos (w - 1)
+
+  constructor
+  · intro h
+    rw [← toInt_inj, toInt_eq_msb_cond] at h
+    have : (intMin w / x).msb = false := by simp [msb_udiv, msb_intMin,  wpos, hx]
+    simp [this, wpos, toInt_intMin] at h
+    omega
+  · intro h
+    subst h
+    simp
+
+theorem intMin_udiv_ne_zero_of_ne_zero {b : BitVec w} (hb : b.msb = false) (hb0 : b ≠ 0#w) :
+    intMin w / b ≠ 0#w := by
+  by_cases hw : w = 0;   subst hw; decide +revert
+  have wpos : 0 < w := by omega
+
+  simp [toNat_eq] at hb0
+  have := @Nat.div_eq_zero_iff_lt b.toNat (2 ^ (w-1)) (by omega)
+  have := toNat_lt_of_msb_false hb
+
+  simp [toNat_eq, wpos]
+  omega
+
+theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1#w) :
+    (a.sdiv b).toInt = a.toInt.tdiv b.toInt := by
+  by_cases hw0 : w = 0;   subst hw0; decide +revert
+  by_cases hw1 : w = 1;   subst hw1; decide +revert
+  by_cases ha0 : a = 0#w; subst ha0; simp
+  by_cases hb0 : b = 0#w; subst hb0; simp
+  by_cases hb1 : b = 1#w; subst hb1; simp [show 1 < w by omega]
+
+  have wpos : 0 < w := by omega
+  have := Nat.two_pow_pos (w - 1)
+
+  by_cases hbintMin : b = intMin w
+  · simp only [ne_eq, Decidable.not_not] at hbintMin
+    subst hbintMin
+    have toIntA_lt := @BitVec.toInt_lt w a; norm_cast at toIntA_lt
+    have le_toIntA := @BitVec.le_toInt w a; norm_cast at le_toIntA
+    simp only [sdiv_intMin, h, ↓reduceIte, toInt_zero, toInt_intMin, wpos,
+      Nat.two_pow_pred_mod_two_pow, Int.tdiv_neg]
+    · by_cases ha_intMin : a = intMin w
+      · simp only [ha_intMin, ↓reduceIte, show 1 < w by omega, toInt_one, toInt_intMin, wpos,
+          Nat.two_pow_pred_mod_two_pow, Int.neg_tdiv, Int.neg_neg]
+        rw [Int.tdiv_self (by omega)]
+      · by_cases ha_nonneg : 0 ≤ a.toInt
+        · simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin]
+        · simp only [ne_eq, ← toInt_inj, toInt_intMin, wpos, Nat.two_pow_pred_mod_two_pow] at h
+          rw [← Int.neg_tdiv, Int.tdiv_eq_zero_of_lt (by omega)]
+          · simp [ha_intMin]
+          · simp [wpos, ← toInt_ne, toInt_intMin] at ha_intMin
+            omega
+
+  · by_cases ha : a.msb <;> by_cases hb : b.msb
+    <;> simp only [not_eq_true] at ha hb
+    · simp only [sdiv_eq, ha, hb, udiv_eq]
+      rw [toInt_eq_neg_toNat_neg_of_nonpos (x := a) (by simp [ha]),
+        toInt_eq_neg_toNat_neg_of_nonpos (x := b) (by simp [hb]),
+        Int.neg_tdiv_neg, Int.tdiv_eq_ediv_of_nonneg (by omega)]
+      rw [toInt_eq_toNat_of_msb]
+      · rfl
+      · by_cases ha_intMin : a = intMin w
+        · simp only [ha_intMin, ne_eq, not_true_eq_false, _root_.false_or] at h
+          simp [msb_udiv, neg_eq_iff_eq_neg, h]
+        · simp [msb_udiv, ha_intMin, ha]
+    · have sdiv_toInt_of_msb_true_of_msb_false :
+          (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]
+          norm_cast
+        · rw [neg_eq_zero_iff]
+          by_cases h' : -a / b = 0#w
+          · simp [h']
+          · by_cases ha_intMin : a = intMin w
+            · have ry := (intMin_udiv_eq_intMin_iff b).mp
+              simp only [hb1, imp_false] at ry
+              simp [msb_udiv, ha_intMin, hb1, ry, intMin_udiv_ne_zero_of_ne_zero, hb, hb0]
+            · have := @BitVec.ne_intMin_of_lt_of_msb_false w ((-a) / b) wpos (by simp [ha, ha0, ha_intMin])
+              simp [msb_neg, h', this, ha, ha_intMin]
+      rw [toInt_eq_toNat_of_msb hb, toInt_eq_neg_toNat_neg_of_msb_true ha, Int.neg_tdiv,
+        Int.tdiv_eq_ediv_of_nonneg (by omega), sdiv_toInt_of_msb_true_of_msb_false]
+    · rw [← @BitVec.neg_neg w (a.sdiv b), ← sdiv_neg hbintMin]
+      have hmb : (-b).msb = false := by simp [hbintMin, hb]
+      rw [toInt_neg_of_ne_intMin]
+      · simp [sdiv, ha, hmb]
+        rw [toInt_udiv_of_msb ha, toInt_eq_toNat_of_msb ha]
+        rw [toInt_eq_neg_toNat_neg_of_msb_true hb, Int.tdiv_neg, Int.tdiv_eq_ediv_of_nonneg (by omega)]
+      · apply sdiv_ne_intMin_of_ne_intMin
+        apply ne_intMin_of_lt_of_msb_false (by omega) ha
+    · rw [sdiv, Int.tdiv_cases, udiv_eq, neg_eq, if_pos (toInt_nonneg_of_msb_false ha),
+        if_pos (toInt_nonneg_of_msb_false hb), ha, hb, toInt_udiv_of_msb ha,
+        toInt_eq_toNat_of_msb ha, toInt_eq_toNat_of_msb hb]
+
+theorem intMin_sdiv_neg_one : (intMin w).sdiv (-1#w) = intMin w := by
+  refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; exact Subsingleton.elim _ _) (fun hw => ?_)
+  apply BitVec.eq_of_toNat_eq
+  rw [sdiv]
+  simp [msb_intMin, hw, negOne_eq_allOnes, msb_allOnes]
+  have : 2 ≤ 2 ^ w := Nat.pow_one 2 ▸ (Nat.pow_le_pow_iff_right (by omega)).2 (by omega)
+  rw [Nat.sub_sub_self (by omega), Nat.mod_eq_of_lt, Nat.div_one]
+  omega
+
+theorem toInt_sdiv (a b : BitVec w) : (a.sdiv b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ w) := by
+  by_cases h : a = intMin w ∧ b = -1#w
+  · rcases h with ⟨rfl, rfl⟩
+    rw [BitVec.intMin_sdiv_neg_one]
+    refine (Nat.eq_zero_or_pos w).elim (by rintro rfl; simp [toInt_of_zero_length]) (fun hw => ?_)
+    rw [toInt_intMin_of_pos hw, negOne_eq_allOnes, toInt_allOnes, if_pos hw, Int.tdiv_neg,
+      Int.tdiv_one, Int.neg_neg, Int.bmod_eq_neg (Int.pow_nonneg (by omega))]
+    conv => lhs; rw [(by omega: w = (w - 1) + 1)]
+    simp [Nat.pow_succ, Int.natCast_pow, Int.mul_comm]
+  · rw [← toInt_bmod_cancel]
+    rw [BitVec.toInt_sdiv_of_ne_or_ne _ _ (by simpa only [Classical.not_and_iff_not_or_not] using h)]
+
 /-! ### Lemmas that use Bitblasting circuits -/
 
 theorem add_sub_comm {x y : BitVec w} : x + y - z = x - z + y := by
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f7843162ef..063c79af5b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -391,6 +391,15 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
   simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h
   rw [Nat.mod_eq_of_lt (by omega)]
 
+@[simp] theorem sub_toNat_mod_cancel_of_toNat {x : BitVec w} (h : x.toNat ≠ 0) :
+    (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
+  by_cases h : w = 0
+  · subst h
+    simp [BitVec.eq_nil x] at h
+  have := x.isLt
+  rw [Nat.mod_eq_of_lt]
+  omega
+
 @[simp] theorem toNat_mod_cancel_of_lt {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by
   have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h
   exact Nat.mod_eq_of_lt (by omega)
@@ -647,6 +656,34 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
 theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
   simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]
 
+@[simp]
+theorem toNat_one (h : 0 < w) : (1#w : BitVec w).toNat = 1 := by
+  simp
+  omega
+
+@[simp]
+theorem toInt_one (h : 1 < w) : (1#w : BitVec w).toInt = 1 := by
+  rw [toInt_eq_toNat_of_msb, toNat_one (by omega)]
+  · simp
+  · simp
+    omega
+
+@[simp] theorem sub_toNat_mod_cancel_of_msb_true {x : BitVec w} (h : x.msb = true) :
+    (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by
+  simp only [msb_eq_decide, ge_iff_le, decide_eq_true_eq] at h
+  have := Nat.two_pow_pos (w-1)
+  exact sub_toNat_mod_cancel_of_toNat (by omega)
+
+theorem toNat_lt_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) : x.toNat < 2 ^ (w - 1) := by
+  have rt := @msb_eq_decide w x
+  simp only [ge_iff_le, false_eq_decide_iff, Nat.not_le, h] at rt
+  omega
+
+theorem le_toNat_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : 2 ^ (w - 1) ≤ x.toNat := by
+  have rt := @msb_eq_decide w x
+  simp only [h, ge_iff_le, true_eq_decide_iff] at rt
+  omega
+
 /--
 `x.toInt` is less than `2^(w-1)`.
 We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
@@ -972,7 +1009,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
 
 @[simp] theorem toInt_extractLsb' {s m : Nat} {x : BitVec n} :
-    (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by 
+    (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by
   simp [extractLsb', toInt_ofNat]
 
 @[simp] theorem toInt_extractLsb {hi lo : Nat} {x : BitVec n} :
@@ -1179,6 +1216,11 @@ theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
   simp
   omega
 
+theorem msb_allOnes (hw : 0 < w) : (allOnes w).msb = true := by
+  rw [msb_eq_true_iff_two_mul_ge, toNat_allOnes]
+  have : 2 ≤ 2 ^ w := Nat.pow_one 2 ▸ (Nat.pow_le_pow_iff_right (by omega)).2 (by omega)
+  omega
+
 /-! ### or -/
 
 @[simp] theorem toNat_or (x y : BitVec v) :
@@ -3161,7 +3203,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
   simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
 
 theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
-    (x.toInt - y.toInt < - 2 ^ (w - 1)) 
+    (x.toInt - y.toInt < - 2 ^ (w - 1))
     ↔ (x.toInt < 0 ∧ 0 ≤ y.toInt ∧ 0 ≤ (x.toInt - y.toInt).bmod (2 ^ w)) := by
   rcases w with _|w
   · simp [of_length_zero]
@@ -3177,7 +3219,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
       omega
 
 theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
-    (2 ^ (w - 1) ≤ x.toInt - y.toInt) 
+    (2 ^ (w - 1) ≤ x.toInt - y.toInt)
     ↔ (0 ≤ x.toInt ∧ y.toInt < 0 ∧ (x.toInt - y.toInt).bmod (2 ^ w) < 0) := by
   rcases w with _|w
   · simp [of_length_zero]
@@ -3301,6 +3343,14 @@ theorem neg_neg {x : BitVec w} : - - x = x := by
 protected theorem neg_inj {x y : BitVec w} : -x = -y ↔ x = y :=
   ⟨fun h => by rw [← @neg_neg w x, ← @neg_neg w y, h], congrArg _⟩
 
+theorem neg_eq_iff_eq_neg {x y : BitVec w} : -x = y ↔ x = -y := by
+  constructor
+  all_goals
+    intro h
+    symm at h
+    subst h
+    simp
+
 theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
   constructor
   all_goals
@@ -3736,7 +3786,8 @@ theorem msb_udiv (x y : BitVec w) :
             ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
           _ < 2 ^ w       := by omega
 
-theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
+@[simp]
+theorem msb_udiv_eq_false_of {x : BitVec w} {y : BitVec w} (h : x.msb = false) :
     (x / y).msb = false := by
   simp [msb_udiv, h]
 
@@ -4610,6 +4661,17 @@ The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `
 theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
   simp [intMin]
 
+@[simp]
+theorem intMin_eq_zero_iff {w : Nat} : intMin w = 0#w ↔ w = 0 := by
+  by_cases h : w = 0
+  · subst h
+    decide +revert
+  · constructor
+    · have := Nat.two_pow_pos (w - 1)
+      simp [toNat_eq, show 0 < w by omega]
+      omega
+    · simp [h]
+
 /--
 The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
@@ -4652,6 +4714,14 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   · simp only [Nat.not_lt, Nat.le_zero_eq] at h
     simp [bitvec_to_nat, h]
 
+@[simp]
+theorem neg_eq_intMin {x : BitVec w} : -x = intMin w ↔ x = intMin w := by
+  rw [← BitVec.neg_inj, neg_neg, neg_intMin]
+
+theorem neg_ne_intMin_inj {x : BitVec w} :
+    -x ≠ intMin w ↔ x ≠ intMin w := by
+  rw [←neg_intMin, neg_ne_iff_ne_neg, neg_neg, neg_intMin]
+
 @[simp]
 theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w := by
   simp [BitVec.abs, bitvec_to_nat]
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 782cb01be4..576e9c7246 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -732,6 +732,22 @@ theorem neg_ediv {a b : Int} : (-a) / b = -(a / b) - if b ∣ a then 0 else b.si
         · have := emod_lt_of_neg a hb
           omega
 
+theorem tdiv_cases (n m : Int) : n.tdiv m =
+    if 0 ≤ n then
+      if 0 ≤ m then n / m else -(n / (-m))
+    else
+      if 0 ≤ m then -((-n) / m) else (-n) / (-m) := by
+  split <;> rename_i hn
+  · split <;> rename_i hm
+    · rw [Int.tdiv_eq_ediv_of_nonneg hn]
+    · rw [Int.tdiv_eq_ediv_of_nonneg hn]
+      simp
+  · split <;> rename_i hm
+    · rw [Int.tdiv_eq_ediv, Int.neg_ediv]
+      simp [hn, Int.neg_sub, Int.add_comm]
+    · rw [Int.tdiv_eq_ediv, Int.neg_ediv, Int.ediv_neg]
+      simp [hn, Int.sub_eq_add_neg, apply_ite Neg.neg]
+
 theorem neg_emod {a b : Int} : (-a) % b = if b ∣ a then 0 else b.natAbs - (a % b) := by
   rw [emod_def, emod_def, neg_ediv, Int.mul_sub, Int.mul_neg]
   split <;> rename_i h
@@ -2269,6 +2285,14 @@ theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2 := by
 theorem bmod_eq_emod_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by
   simp [bmod, hx]
 
+theorem bmod_eq_neg {n : Nat} {m : Int} (hm : 0 ≤ m) (hn : n = 2 * m) : m.bmod n = -m := by
+  by_cases h : m = 0
+  · subst h; simp
+  · rw [Int.bmod_def, hn, if_neg]
+    · rw [Int.emod_eq_of_lt hm] <;> omega
+    · simp only [Int.not_lt]
+      rw [Int.emod_eq_of_lt hm] <;> omega
+
 theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
   refine lt_add_one_iff.mp ?_
   calc
diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean
index 4d2f0da343..fb34dd01ca 100644
--- a/src/Init/Data/Int/Pow.lean
+++ b/src/Init/Data/Int/Pow.lean
@@ -17,6 +17,16 @@ protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
+protected theorem pow_pos {n : Int} {m : Nat} : 0 < n → 0 < n ^ m := by
+  induction m with
+  | zero => simp
+  | succ m ih => exact fun h => Int.mul_pos (ih h) h
+
+protected theorem pow_nonneg {n : Int} {m : Nat} : 0 ≤ n → 0 ≤ n ^ m := by
+  induction m with
+  | zero => simp
+  | succ m ih => exact fun h => Int.mul_nonneg (ih h) h
+
 @[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
 abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left