diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 9f35e7b4a381..b7e8ceb3c36e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2152,8 +2152,11 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
 
 @[simp]
 theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
-  apply eq_of_toNat_eq
-  simp [toNat_mul]
+  simp [bv_toNat]
+
+@[simp]
+theorem BitVec.zero_mul {x : BitVec w} : 0#w * x = 0#w := by
+  simp [bv_toNat]
 
 theorem BitVec.mul_add {x y z : BitVec w} :
     x * (y + z) = x * y + x * z := by
@@ -2640,6 +2643,8 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
 
 /- ## twoPow -/
 
+#check Nat.two_pow_pred_mod_two_pow
+
 @[simp, bv_toNat]
 theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
   rcases w with rfl | w
@@ -2681,11 +2686,10 @@ theorem getMsbD_twoPow {i j w: Nat} :
 
 @[simp]
 theorem msb_twoPow {i w: Nat} :
-    (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by
-  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
+    (BitVec.twoPow w i).msb = decide (i + 1 = w) := by
+  simp only [BitVec.msb, BitVec.getMsbD_eq_getLsbD, Nat.sub_zero, BitVec.getLsbD_twoPow,
     Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
-  intros
-  omega
+  by_cases h : i + 1 = w <;> simp [h] <;> omega
 
 theorem and_twoPow (x : BitVec w) (i : Nat) :
     x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
@@ -3035,6 +3039,364 @@ instance instDecidableExistsBitVec :
     have := instDecidableExistsBitVec n
     inferInstance
 
+theorem div_twoPow_div_twoPow_eq_mul {n m : Nat} (x : BitVec w) :
+    x / (BitVec.twoPow w n) / (BitVec.twoPow w m) =
+      x / ((BitVec.twoPow w n) * (BitVec.twoPow w m)) := by
+  simp only [BitVec.toNat_eq, BitVec.toNat_udiv, BitVec.toNat_twoPow, BitVec.toNat_mul,
+    Nat.mul_mod_mod, Nat.mod_mul_mod]
+  by_cases hzz : x = 0
+  · subst hzz
+    simp
+  · by_cases h : n + m < w
+    ·
+      have hl : 2^n * 2^m < 2^w := by
+        rw [← Nat.pow_add]
+        have asdd := (@Nat.pow_lt_pow_iff_right 2 (n + m) w (by omega)).mpr h
+        apply asdd
+      simp [Nat.mod_eq_of_lt hl]
+      have := @Nat.mul_lt_mul_of_le_of_lt
+      have := @Nat.mul_lt_mul_right (2 ^ n) (2 ^ m) (2 ^ w) (by apply Nat.two_pow_pos)
+      have := @Nat.lt_of_mul_lt (2^n) (2^m) (2^w) (by apply Nat.two_pow_pos) h
+      rw [Nat.mul_comm] at hl
+      have := @Nat.lt_of_mul_lt (2^m) (2^n) (2^w) (by apply Nat.two_pow_pos) h
+      have : 2 ^ m < 2 ^ w := by omega
+      simp [Nat.mod_eq_of_lt, *]
+      rw [Nat.div_div_eq_div_mul]
+    ·
+      rw [←Nat.pow_add]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      simp [h]
+      by_cases h₄ : n < w
+      · by_cases h₅ : m < w
+        · simp [h₄, h₅]
+          simp at h
+          rw [Nat.div_div_eq_div_mul]
+          rw [←Nat.pow_add]
+          rw [Nat.div_eq_zero_iff]
+          have xzero := BitVec.isLt x
+          simp [bv_toNat] at hzz
+          have := @Nat.pow_pos 2 w (by omega)
+          have : 2 ^ w ≤ 2 ^ (n + m) := by
+            apply Nat.pow_le_pow_of_le (by omega) h
+          omega
+          have := @Nat.pow_pos 2 (n + m) (by omega)
+          omega
+        · simp [h₄, h₅]
+      · by_cases h₅ : m < w
+        · simp [h₄, h₅]
+        · simp [h₄, h₅]
+
+theorem udiv_twoPow {n : Nat} {x : BitVec w} :
+    x / (BitVec.twoPow w n) = x >>> n := by
+  simp only [BitVec.toNat_eq, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow,
+    BitVec.toNat_udiv, BitVec.toNat_twoPow]
+  by_cases h : n < w
+  · rw [Nat.mod_eq_of_lt ((Nat.pow_lt_pow_iff_right (by omega)).mpr h)]
+  · by_cases hh : x.toNat = 0
+    · simp [hh]
+    · have : 2 ^ w ≤ 2 ^ n := (Nat.pow_le_pow_iff_right (by omega)).mpr (by omega)
+      rw [(@Nat.div_eq_zero_iff (2 ^ n) x.toNat (by omega)).mpr (by omega),
+        Nat.mod_eq_zero_of_dvd, Nat.div_zero]
+      apply Nat.pow_dvd_pow 2 (by omega)
+
+theorem aaas (x y : BitVec w) : -(x / -y) = x / y := by
+  simp [bv_toNat]
+  by_cases h : y = 0
+  · subst h
+    simp
+  · rw [Nat.mod_eq_of_lt (a := 2 ^ w - y.toNat)]
+    · rw [Nat.mul_div_mul_left]
+
+      sorry
+    · have := isLt y
+      simp only [ofNat_eq_ofNat, toNat_eq, toNat_ofNat, Nat.zero_mod] at h
+      omega
+
+theorem twoPow_large (h : i ≥ w): (twoPow w i) = 0#w := by
+  simp only [toNat_eq, toNat_twoPow, toNat_ofNat, Nat.zero_mod]
+  rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+  simp [h]
+  omega
+
+theorem twoPow_neg_large : (-(twoPow (w+1) (w))) = twoPow (w+1) w := by
+  simp [toNat_eq, toNat_twoPow, toNat_ofNat, Nat.zero_mod]
+  rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+  have h : ¬ (w + 1 < w) := by omega
+  simp [h]
+  have le := @Nat.two_pow_sub_two_pow_pred (w+1) (by omega)
+  simp at le
+  apply le
+
+def testaa : Bool := Id.run do
+  for xv in [0, 1, 2, 3, 4, 5, 6, 7, 8] do
+    for w in [1, 2, 3, 4] do
+      for n in [0, 1, 2, 3, 4, 5] do
+        let x := BitVec.ofNat w xv
+        if x.sdiv (BitVec.twoPow w n) ≠ (if n +1 < w then x.sshiftRight n else if n + 1 = w then 1#w else 0#w) then
+          return False
+  return True
+
+#eval testaa
+
+#eval (8#4).sdiv (8#4)
+
+theorem udiv_eq_one {x y : BitVec w} : x / y = 1#w := by
+  simp [bv_toNat]
+  rw [Nat.div_]
+  sorry
+
+theorem sdiv_twoPow' {n : Nat} {x : BitVec w} (hmsb : x.msb = false) (hn : ¬ (n + 1 = w)) :
+    x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by
+  simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq]
+  simp only [hmsb, hn, decide_False]
+  rw [BitVec.sshiftRight_eq_of_msb_false hmsb]
+  rw [udiv_twoPow]
+
+/-
+0x0#4
+-/
+#eval (7#4).sshiftRight 3
+/-
+0x8#4
+-/
+#eval (twoPow 4 3)
+/-
+0x0#4
+-/
+#eval (7#4).sdiv (twoPow 4 3)
+
+theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (h : n ≥ w) :
+    x >>> n = 0#w := by
+  simp [bv_toNat]
+  rw [Nat.shiftRight_eq_div_pow]
+  rw [Nat.div_eq]
+  have rt := isLt x
+  have re := @Nat.pow_le_pow_of_le 2 w n (by omega) (by omega)
+  by_cases h₂ : 0 < 2 ^ n ∧ 2 ^ n ≤ x.toNat
+  · omega
+  · simp [h₂]
+
+theorem ushiftRight_eq_zero_of_msb_false {x : BitVec w} {n : Nat} (h : n + 1 = w) (h₂ : x.msb = false) :
+    x >>> n = 0#w := by
+  simp [bv_toNat]
+  rw [Nat.shiftRight_eq_div_pow]
+  rw [Nat.div_eq]
+  have rt := isLt x
+  have re := @Nat.pow_le_pow_of_le 2 w (n+1) (by omega) (by omega)
+  by_cases h₃ : 0 < 2 ^ n ∧ 2 ^ n ≤ x.toNat
+  · simp [h₃]
+    have sr := (@BitVec.msb_eq_false_iff_two_mul_lt w x).mp h₂
+    omega
+  · simp [h₃]
+
+
+theorem sdiv_twoPow₂ {n : Nat} {x : BitVec w} (hmsb : x.msb = false) (hn : n + 1 = w) :
+    x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by
+  simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq]
+  simp only [hmsb, hn, decide_True]
+  rw [BitVec.sshiftRight_eq_of_msb_false hmsb]
+  symm at hn
+  subst hn
+  rw [twoPow_neg_large]
+  rw [udiv_twoPow]
+  rw [ushiftRight_eq_zero_of_msb_false]
+  simp
+  simp
+  simp [hmsb]
+
+theorem sdiv_twoPow_of_msb_true {n : Nat} {x : BitVec w} (h : x.msb = true) (h2 : n + 1 = w) (h3 : 2 ^ n = x.toNat) :
+    x.sdiv (BitVec.twoPow w n) = 1#w := by
+  by_cases hw : w = 0
+  · subst hw
+    simp [twoPow]
+  · have re : 0 < w := by omega
+    simp [BitVec.sdiv]
+    simp [*, bv_toNat]
+    rw [Nat.div_self]
+    by_cases hy : x.toNat = 0
+    · have lr := @Nat.pow_pos 2 n (by omega)
+      omega
+    · rw [Nat.mod_eq_of_lt]
+      omega
+      omega
+
+theorem sdiv_twoPow_of_msb_true' {n : Nat} {x : BitVec w} (h : x.msb = true) (h2 : n + 1 = w) (h3 : 2 ^ n > x.toNat) :
+    x.sdiv (BitVec.twoPow w n) = 1#w := by
+  by_cases hw : w = 0
+  · subst hw
+    simp [twoPow]
+  · have re : 0 < w := by omega
+    simp [BitVec.sdiv]
+    simp [*, bv_toNat]
+    have lr := @Nat.pow_pos 2 n (by omega)
+    have lr := @Nat.pow_pos 2 w (by omega)
+    symm at h2
+    subst h2
+    by_cases hy : x.toNat = 0
+    · have le := (@BitVec.msb_eq_true_iff_two_mul_ge (n+1) x).mp h
+      rw [Nat.mul_comm] at le
+      rw [Nat.mul_two] at le
+      omega
+    ·
+      rw [Nat.mod_eq_of_lt (by omega)]
+      have tl := @Nat.two_pow_pred_mod_two_pow (n + 1) (by omega)
+      simp at tl
+      rw [tl]
+      have tl := @Nat.two_pow_sub_two_pow_pred (n + 1) (by omega)
+      simp at tl
+      rw [tl]
+      have tl := @Nat.two_pow_pred_mod_two_pow (n + 1) (by omega)
+      simp at tl
+      rw [tl]
+      rw [Nat.div_eq_zero_iff]
+      rw [Nat.div_eq]
+      simp [*]
+
+      Omega
+
+theorem xxr {x : BitVec w} (h : x.msb = false) : - (x >>> 1) = (-x).sshiftRight 1 := by
+  ext
+  rw [getLsbD_sshiftRight]
+  rw [getLsbD_neg]
+  rw [getLsbD_ushiftRight]
+
+
+  induction w
+  case zero =>
+    simp [BitVec.eq_nil x]
+  case succ i ih =>
+
+
+
+
+
+
+
+  sorry
+
+theorem sdiv_twoPow_msb {n : Nat} {x : BitVec w} (h : x.msb = true) (h2 : n +1 < w) :
+    x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by
+  simp [sdiv]
+  have rr : ¬ (n + 1 = w) := by omega
+  simp [*]
+  rw [udiv_twoPow]
+  induction n
+  · simp
+  case succ i ih =>
+    have hr := @ih (by omega) (by omega)
+    rw [sshiftRight_add]
+    rw [← hr]
+    rw [shiftRight_add]
+    congr
+    rw [xxr]
+    have rr : (-x).msb = false := by
+      sorry
+    have rr2 : ((-x) >>> i).msb = false := by
+      sorry
+    simp [rr2]
+
+
+theorem sdiv_twoPow {n : Nat} {x : BitVec w} :
+    x.sdiv (BitVec.twoPow w n) = if x.msb = false ∨ n < w then x.sshiftRight n else 0#w := by
+  by_cases hhh : x.msb = false
+  · by_cases hr : n + 1 = w
+    · simp [hhh]
+      rw [sdiv_twoPow₂ hhh hr]
+    · simp [hhh]
+      rw [sdiv_twoPow' hhh hr]
+  · simp [hhh]
+    by_cases ha : n ≥ w
+    · simp [show ¬ (n < w) by omega]
+      rw [twoPow_large ha]
+      simp
+    · by_cases hrr : n + 1 < w
+      ·
+        simp [show (n < w) by omega]
+        rw [sdiv_twoPow_msb]
+        simp at hhh
+        simp [hhh]
+        omega
+      · simp_all
+        have lr : w = n + 1 := by omega
+        subst lr
+        clear ha hrr
+        sorry
+
+theorem sdiv_twoPow''' {n : Nat} {x : BitVec w} :
+    x.sdiv (BitVec.twoPow w n) = if n + 1 < w then x.sshiftRight n else if n + 1 = w then 1#w else 0#w := by
+  by_cases hb : n + 1 = w
+  · simp [hb]
+    by_cases ha : n ≥ w
+    · sorry
+    · simp_all
+      have : w = n + 1 := by omega
+      subst this
+      rw [BitVec.sdiv]
+      by_cases hhh : x.msb
+      · simp [hhh, bv_toNat]
+        have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega)
+        simp at this
+        rw [this]
+        have := @Nat.two_pow_sub_two_pow_pred (n+1) (by omega)
+        simp at this
+        rw [this]
+        have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega)
+        simp at this
+        rw [this]
+        have el := (@BitVec.msb_eq_true_iff_two_mul_ge (n+1) x).mp hhh
+        rw [Nat.mul_comm] at el
+        rw [Nat.mul_two] at el
+        have lr := @Nat.two_pow_pred_add_two_pow_pred (n+1) (by omega)
+        simp at lr
+        symm at lr
+        rw [← Nat.mul_two] at lr
+        rw [← Nat.mul_two] at el
+        rw [lr] at el
+        simp at el
+        by_cases rt : 2 ^ n = x.toNat
+        · symm at rt
+          rw [rt]
+          have as := @Nat.two_pow_sub_two_pow_pred (n+1) (by omega)
+          simp at as
+          rw [as]
+          have aadd := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega)
+          simp at aadd
+          rw [aadd]
+          rw [Nat.div_self]
+          apply Nat.pow_pos
+          omega
+
+        · have ar : 2 ^ n < x.toNat := by omega
+          by_cases rl : x.toNat  = 2^(n+1)
+          ·
+            simp [rl]
+          ·
+            rw [Nat.mod_eq_of_lt (by omega)]
+            rw [Nat.div_eq_zero_iff (by omega)]
+            have := @Nat.two_pow_pred_add_two_pow_pred (n+1) (by omega)
+            simp at this
+            rw [←this]
+            simp
+            omega
+
+      · simp [hhh, bv_toNat]
+        have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega)
+        simp at this
+        rw [this]
+        have := @Nat.two_pow_sub_two_pow_pred (n+1) (by omega)
+        simp at this
+        rw [this]
+        have := @Nat.two_pow_pred_mod_two_pow (n+1) (by omega)
+        simp at this
+        rw [this]
+        rw [Nat.div_eq_zero_iff]
+        simp at hhh
+        · have el := (@BitVec.msb_eq_false_iff_two_mul_lt (n+1) x).mp hhh
+          omega
+        · apply Nat.two_pow_pos
+
 /-! ### Deprecations -/
 
 set_option linter.missingDocs false
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 0aa6a9ae9e72..0fd972cc580c 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -549,6 +549,12 @@ protected theorem mul_left_cancel_iff {n : Nat} (p : 0 < n) {m k : Nat} : n * m
 protected theorem mul_right_cancel_iff {m : Nat} (p : 0 < m) {n k : Nat} : n * m = k * m ↔ n = k :=
   ⟨Nat.mul_right_cancel p, fun | rfl => rfl⟩
 
+protected theorem mul_left_inj (ha : a ≠ 0) : b * a = c * a ↔ b = c :=
+  Nat.mul_right_cancel_iff (Nat.pos_iff_ne_zero.2 ha)
+
+protected theorem mul_right_inj (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
+  Nat.mul_left_cancel_iff (Nat.pos_iff_ne_zero.2 ha)
+
 protected theorem ne_zero_of_mul_ne_zero_right (h : n * m ≠ 0) : m ≠ 0 :=
   (Nat.mul_ne_zero_iff.1 h).2
 
@@ -664,6 +670,9 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
 @[simp] theorem add_mod_mod (m n k : Nat) : (m + n % k) % k = (m + n) % k := by
   rw [Nat.add_comm, mod_add_mod, Nat.add_comm]
 
+@[simp] theorem mul_mod_mod (a b c : Nat) : (a * (b % c)) % c = a * b % c := by
+  rw [mul_mod, mod_mod, ← mul_mod]
+
 theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
   rw [add_mod_mod, mod_add_mod]
 
@@ -894,6 +903,11 @@ protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a
     a / b = c ↔ a = c * b := by
   rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
 
+protected theorem div_eq_zero_iff (hb : 0 < b) : a / b = 0 ↔ a < b where
+  mp h := by rw [← mod_add_div a b, h, Nat.mul_zero, Nat.add_zero]; exact mod_lt _ hb
+  mpr h := by rw [← Nat.mul_right_inj (Nat.ne_of_gt hb), ← Nat.add_left_cancel_iff, mod_add_div,
+      mod_eq_of_lt h, Nat.mul_zero, Nat.add_zero]
+
 theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
     ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
   | x + 1, w => by
@@ -923,6 +937,17 @@ protected theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a
     rw [Nat.pow_add]
     apply Nat.dvd_mul_right
 
+protected theorem two_pow_mod_two_pow_iff {b m n : Nat} (h : 1 < b):
+    (b ^ n % b ^ m) = if n < m then b ^ n else 0 := by
+  by_cases h : n < m
+  · simp only [h, ↓reduceIte]
+    apply Nat.mod_eq_of_lt
+    apply Nat.pow_lt_pow_of_lt (by omega) h
+  · simp only [h, ↓reduceIte]
+    simp only [Nat.not_lt] at h
+    apply Nat.mod_eq_zero_of_dvd
+    apply Nat.pow_dvd_pow b (by omega)
+
 protected theorem pow_sub_mul_pow (a : Nat) {m n : Nat} (h : m ≤ n) :
     a ^ (n - m) * a ^ m = a ^ n := by
   rw [← Nat.pow_add, Nat.sub_add_cancel h]
diff --git a/src/Init/Data/Nat/Mod.lean b/src/Init/Data/Nat/Mod.lean
index 2ef6691913aa..3ced86c318dc 100644
--- a/src/Init/Data/Nat/Mod.lean
+++ b/src/Init/Data/Nat/Mod.lean
@@ -21,6 +21,17 @@ which should probably be moved to their own file.
 
 namespace Nat
 
+protected theorem lt_of_mul_lt {a b c : Nat} (h : 0 < b) (h₂ : a * b < c) : a < c := by
+  induction a generalizing c
+  case zero =>
+    simp only [Nat.zero_mul] at h₂
+    simp [h₂]
+  case succ i ih =>
+    simp only [Nat.add_mul, Nat.one_mul] at h₂
+    apply Nat.add_lt_of_lt_sub
+    apply ih
+    omega
+
 @[simp] protected theorem mul_lt_mul_left (a0 : 0 < a) : a * b < a * c ↔ b < c := by
   induction a with
   | zero => simp_all