From 38ef4e4794e527e8e4c1d6505490a8aa58e8b32e Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Thu, 7 Nov 2024 15:16:12 -0800
Subject: [PATCH 01/19] feat: BitVec.toFin/toInt (BitVec.ushiftRight x)

Unsigned shift right by at least one bit makes the value of the bitvector less than or equal to `2^(w-1)`,
makes the interpretation of the bitvector `Int` and `Nat` agree.
In the case when `n = 0`, then the shift right value equals the integer interpretation.

```lean
theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
    (x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n
```

---

```lean
theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
    (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n))
```

Co-authored-by: Harun Khan <harun19@stanford.edu>
---
 src/Init/Data/BitVec/Lemmas.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1cf870d30dfb..4603e31337a1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1616,7 +1616,7 @@ because it makes the value of the bitvector less than or equal to `2^(w-1)`.
 In the case when `n = 0`, then the shift right value equals the integer interpretation.
 -/
 @[simp]
-theorem toInt_ushiftRight {x : BitVec w} {n : Nat} :
+theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
     (x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n := by
   by_cases hn : n = 0
   · simp [hn]
@@ -1626,12 +1626,12 @@ theorem toInt_ushiftRight {x : BitVec w} {n : Nat} :
 @[simp]
 theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
     (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n)) := by
-  apply Fin.eq_of_val_eq
-  by_cases hn : n < w
-  · simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)]
-  · simp only [Nat.not_lt] at hn
-    rw [ushiftRight_eq_zero (by omega)]
-    simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]
+    apply Fin.eq_of_val_eq
+    by_cases hn : n < w
+    · simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)]
+    · simp only [Nat.not_lt] at hn
+      rw [ushiftRight_eq_zero (by omega)]
+      simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]
 
 @[simp]
 theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :

From 49f4cfa177c717b788257ac373c8177bd775cbe2 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Fri, 29 Nov 2024 20:30:53 +0000
Subject: [PATCH 02/19] Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Tobias Grosser <github@grosser.es>
---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 4603e31337a1..a329ca965fe8 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1616,7 +1616,7 @@ because it makes the value of the bitvector less than or equal to `2^(w-1)`.
 In the case when `n = 0`, then the shift right value equals the integer interpretation.
 -/
 @[simp]
-theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
+theorem toInt_ushiftRight {x : BitVec w} {n : Nat} :
     (x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n := by
   by_cases hn : n = 0
   · simp [hn]

From 5ee463edeaaca6ff128e11cb8e807e20417ad0cb Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Fri, 29 Nov 2024 20:31:07 +0000
Subject: [PATCH 03/19] Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Tobias Grosser <github@grosser.es>
---
 src/Init/Data/BitVec/Lemmas.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a329ca965fe8..1cf870d30dfb 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1626,12 +1626,12 @@ theorem toInt_ushiftRight {x : BitVec w} {n : Nat} :
 @[simp]
 theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
     (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n)) := by
-    apply Fin.eq_of_val_eq
-    by_cases hn : n < w
-    · simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)]
-    · simp only [Nat.not_lt] at hn
-      rw [ushiftRight_eq_zero (by omega)]
-      simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]
+  apply Fin.eq_of_val_eq
+  by_cases hn : n < w
+  · simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)]
+  · simp only [Nat.not_lt] at hn
+    rw [ushiftRight_eq_zero (by omega)]
+    simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]
 
 @[simp]
 theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :

From 12757f1d7ac2ea32a518103533e8fe8893cd2408 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 1 Dec 2024 14:38:47 -0800
Subject: [PATCH 04/19] progress

---
 src/Init/Data/BitVec/Lemmas.lean    | 23 +++++++++++++++++++++++
 src/Init/Data/Int/DivModLemmas.lean | 20 ++++++++++++++++++++
 2 files changed, 43 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1cf870d30dfb..becbc7ef1de9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1741,6 +1741,29 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
     apply BitVec.lt_of_getLsbD hlsb
   · simp [sshiftRight_eq_of_msb_true hmsb]
 
+
+#eval ((14#4).sshiftRight 0).toInt
+#eval ((14#4).toInt >>> 0)
+
+#check Int.bmod_lt
+#check Int.bmod
+#check Int.mod_eq_of_lt
+
+#eval ((7#4).toInt).bmod 16
+#eval (9#4).toInt >>>1
+
+
+
+@[simp]
+theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
+    (x.sshiftRight n).toInt = x.toInt >>> n := by
+    simp only [BitVec.sshiftRight, toInt_ofInt]
+    rw [Int.bmod_eq_of_lt]
+    rw [Int.emod_eq_of_lt]
+    norm_cast
+    rw [Nat.mod_eq_of_lt]
+    sorry
+
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
   ext i
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index d1003f1559f7..4fb502571064 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -547,6 +547,23 @@ theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
 
 theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
   have b0 := Int.le_trans H1 (Int.le_of_lt H2)
+  match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
+
+#check Int.ediv_eq_zero_of_lt
+#eval (-3)/10
+#eval (-3)%10
+
+theorem emod_eq_of_gt_lt {a b : Int} (H1 : -b < a) (H2 : a < b) : a % b = a := by
+  rw [Int.emod_def]
+  have : a/b = 0 := by
+    simp [Int.ediv_]
+  rw [natAbs_eq_zero] at this
+  simp [this]
+
+
+
+
   match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
 
@@ -1287,6 +1304,9 @@ theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2 := by
       exact Int.sub_neg_of_lt this
     · exact Int.le.intro_sub _ rfl
 
+theorem bmod_eq_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by
+  simp [bmod, hx]
+
 theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
   refine lt_add_one_iff.mp ?_
   calc

From 6106907cf0f6a78dbb7cc46c784770d083abe243 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 1 Dec 2024 19:27:55 -0800
Subject: [PATCH 05/19] progres

---
 src/Init/Data/BitVec/Lemmas.lean    | 30 ++++++++++++++++++-----------
 src/Init/Data/Int/DivModLemmas.lean | 22 ++++++++++-----------
 2 files changed, 30 insertions(+), 22 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index becbc7ef1de9..4f1c6321ce11 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1742,27 +1742,35 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
   · simp [sshiftRight_eq_of_msb_true hmsb]
 
 
-#eval ((14#4).sshiftRight 0).toInt
-#eval ((14#4).toInt >>> 0)
+#eval ((6#4).sshiftRight 4).toInt
+#eval ((6#4).toInt >>> 4)
+
+
+
 
 #check Int.bmod_lt
 #check Int.bmod
 #check Int.mod_eq_of_lt
 
-#eval ((7#4).toInt).bmod 16
+#eval ((9#4).toInt).bmod 16
 #eval (9#4).toInt >>>1
-
-
+#eval (-4) % 16
+#check Int.bmod_lt
 
 @[simp]
 theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
     (x.sshiftRight n).toInt = x.toInt >>> n := by
-    simp only [BitVec.sshiftRight, toInt_ofInt]
-    rw [Int.bmod_eq_of_lt]
-    rw [Int.emod_eq_of_lt]
-    norm_cast
-    rw [Nat.mod_eq_of_lt]
-    sorry
+    simp only [BitVec.sshiftRight, toInt_ofInt, Int.bmod]
+    split
+    · rw [← Int.bmod_eq_of_lt, ← show (x >>> n).toInt = x.toInt >>> n by rfl]
+      rw [toInt_eq_toNat_bmod, Int.bmod_bmod]
+      assumption
+    · sorry
+    -- rw [Int.bmod_eq_of_lt]
+    -- rw [Int.emod_eq_of_lt]
+    -- norm_cast
+    -- rw [Nat.mod_eq_of_lt]
+    -- sorry
 
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 4fb502571064..3c471d06ca6a 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -550,22 +550,22 @@ theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
   match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
 
-#check Int.ediv_eq_zero_of_lt
-#eval (-3)/10
-#eval (-3)%10
+-- #check Int.ediv_eq_zero_of_lt
+-- #eval (-3)/10
+-- #eval (-3)%10
 
-theorem emod_eq_of_gt_lt {a b : Int} (H1 : -b < a) (H2 : a < b) : a % b = a := by
-  rw [Int.emod_def]
-  have : a/b = 0 := by
-    simp [Int.ediv_]
-  rw [natAbs_eq_zero] at this
-  simp [this]
+-- theorem emod_eq_of_gt_lt {a b : Int} (H1 : -b < a) (H2 : a < b) : a % b = a := by
+--   rw [Int.emod_def]
+--   have : a/b = 0 := by
+--     simp [Int.ediv_]
+--   rw [natAbs_eq_zero] at this
+--   simp [this]
 
 
 
 
-  match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
+  -- match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
+  -- | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
 
 @[simp] theorem emod_self_add_one {x : Int} (h : 0 ≤ x) : x % (x + 1) = x :=
   emod_eq_of_lt h (Int.lt_succ x)

From 8ba58caa9119b20caad6f6b38cf5d9ce1a09a0a1 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sat, 7 Dec 2024 22:00:06 -0800
Subject: [PATCH 06/19] more attempst

---
 src/Init/Data/BitVec/Lemmas.lean     | 99 +++++++++++++++++++++++++---
 src/Init/Data/Nat/Bitwise/Basic.lean |  4 ++
 2 files changed, 93 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 4f1c6321ce11..c04aee042c81 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -582,6 +582,23 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
     0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
   simp [toInt_eq_toNat_cond]; omega
 
+theorem toInt_lt {w : Nat} {x : BitVec w} : BitVec.toInt x < 2^w := by
+  simp only [toInt_eq_toNat_cond]
+  split
+  · norm_cast; simp [x.isLt]
+  · apply Int.lt_trans (Int.sub_lt_self _ (by norm_cast; apply Nat.two_pow_pos w))
+                       (by norm_cast; exact x.isLt)
+
+theorem toInt_gt {w : Nat} {x : BitVec w} : -2^w < BitVec.toInt x := by
+  simp only [toInt_eq_toNat_cond]
+  split
+  · apply Int.lt_of_lt_of_le (by apply Int.neg_neg_of_pos; norm_cast; exact Nat.two_pow_pos w)
+                             (by norm_cast; simp)
+  · norm_cast
+    rw [Int.sub_eq_add_neg]
+    apply Int.lt_add_of_pos_left
+    omega
+
 theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
   obtain ⟨a, ha⟩ := a
   simp only [Nat.reducePow]
@@ -1748,24 +1765,86 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
 
 
 
-#check Int.bmod_lt
-#check Int.bmod
-#check Int.mod_eq_of_lt
+#check Int.emod_def
+#check Int.neg_tdiv
+#check toInt_neg_iff
+
+
+#eval (-7)/16
+
 
 #eval ((9#4).toInt).bmod 16
 #eval (9#4).toInt >>>1
-#eval (-4) % 16
+#eval (-15) % 16
+#eval (-7) % 16
 #check Int.bmod_lt
+#eval (9#4).toInt
+#eval ((10#4) >>>1).toInt
+#eval 8 >>> 0
 
+-- when is x % 2^w - 2^w = x for integers x
+-- when is x % 2^w = x for integers
+
+#check Int.ediv_eq_zero_of_lt
+#check Int.neg_ofNat_succ
+#check Int.neg_emod
+#check Int.emod_def
+#eval (-3)/5
+#eval -(3/5)
+
+example (a b : Int) (h : b  < 0) (h1 : a ≤ 0): ∃ m, b = Int.negSucc m  := by
+  exact Int.eq_negSucc_of_lt_zero h
+
+#check Int.ediv_neg
+example ( a b c : Int) : a/b/c = a/(b*c) := by
+
+
+theorem toInt_shiftRights {x : BitVec w} (n : Nat) (h : n ∣ a) :
+  x.toInt >>> n = if 2*x.toNat < 2^w then x.toNat >>> n else x.toNat >>> n - 2^n := by
+  simp [toInt_eq_toNat_cond, Int.shiftRight_eq_div_pow]
+  rw [Int.bmod_def]
+  norm_cast
+  split
+  · split
+    · exact?
+
+
+#eval (-19 : Int) >>> 0
 @[simp]
 theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
     (x.sshiftRight n).toInt = x.toInt >>> n := by
-    simp only [BitVec.sshiftRight, toInt_ofInt, Int.bmod]
-    split
-    · rw [← Int.bmod_eq_of_lt, ← show (x >>> n).toInt = x.toInt >>> n by rfl]
-      rw [toInt_eq_toNat_bmod, Int.bmod_bmod]
-      assumption
-    · sorry
+    simp only [BitVec.sshiftRight, toInt_ofInt]
+    by_cases h : 2 * x.toNat < 2^w
+    · have := Nat.lt_of_le_of_lt (Nat.shiftRight_le x.toNat n) x.isLt
+      have h2 : (x.toNat >>> n) % 2^w < (2^w + 1)/2 := by sorry
+      simp only [toInt_eq_toNat_cond, h, Int.natCast_shiftRight, ite_true]
+      norm_cast
+      simp only [h2, ite_true, Int.ofNat_emod]
+      rw [Int.emod_eq_of_lt (by norm_cast; simp) (by norm_cast)]
+    · have h0 : x.toInt < 0 := by
+        simp only [toInt_eq_toNat_cond, h, ite_false]
+        apply Int.sub_neg_of_lt (by norm_cast; simp [x.isLt])
+      have h1 := Int.ediv_neg' (b := 2^n) h0 (by norm_cast; exact Nat.two_pow_pos n)
+      have ⟨a, ha⟩ := Int.eq_negSucc_of_lt_zero h1
+      have ha1 : a < 2^w := sorry
+      have h2 := Int.ofNat_le.mpr (Int.natAbs_div_le_natAbs x.toInt (2^n))
+      simp only [Int.ofNat_natAbs_of_nonpos _,
+                 Int.le_of_lt h1, Int.le_of_lt h0] at h2
+      have h3 : x.toInt ≥ -2^w/2 := by
+        simp only [toInt_eq_toNat_cond, h, ite_false]
+        norm_cast; omega
+      have h4 : ¬ Int.negSucc a + 2^w < (2^w + 1) /2 := by
+        simp only [Int.not_lt, Nat.not_lt] at *
+        rw [← ha]
+        have : 2^w/2 ≤ (2^w+1)/2 := sorry
+        omega
+      rw [Int.emod_def, Int.shiftRight_eq_div_pow]
+      push_cast
+      rw [ha, Int.negSucc_ediv _ (by norm_cast; exact Nat.two_pow_pos w),
+          ← show ∀ a b, a/b = Int.ediv a b by intros; rfl,
+          Int.ediv_eq_zero_of_lt (by norm_cast; simp) (by norm_cast)]
+      simp [h4]
+
     -- rw [Int.bmod_eq_of_lt]
     -- rw [Int.emod_eq_of_lt]
     -- norm_cast
diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean
index dde8c2624718..cd1d86f45a0b 100644
--- a/src/Init/Data/Nat/Bitwise/Basic.lean
+++ b/src/Init/Data/Nat/Bitwise/Basic.lean
@@ -74,6 +74,10 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
 theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0 := by
   simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn]
 
+theorem shiftRight_le (m n : Nat) : m >>> n ≤ m := by
+  simp [Nat.shiftRight_eq_div_pow]
+  apply Nat.div_le_self
+
 /-!
 ### testBit
 We define an operation for testing individual bits in the binary representation

From facda43a7faf3837a009b680f8c4ebb486df20d4 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Mon, 9 Dec 2024 11:13:12 -0800
Subject: [PATCH 07/19] progress

---
 src/Init/Data/BitVec/Lemmas.lean    | 30 +++++++++++++++--------------
 src/Init/Data/Int/DivModLemmas.lean | 11 +++++++++++
 2 files changed, 27 insertions(+), 14 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index c04aee042c81..01b518104324 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1795,23 +1795,26 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
 example (a b : Int) (h : b  < 0) (h1 : a ≤ 0): ∃ m, b = Int.negSucc m  := by
   exact Int.eq_negSucc_of_lt_zero h
 
-#check Int.ediv_neg
-example ( a b c : Int) : a/b/c = a/(b*c) := by
+#check Nat.div_lt_self
+example ( a b c : Int) : a/b/c = a/(b*c) := sorry
 
+example ( a b c : Int) (h : 0 < b) : (a/b).natAbs < a.natAbs := by
+  push_cast
+  simp only [Int.natAbs_ediv, Int.natAbs_lt_natAbs]
 
-theorem toInt_shiftRights {x : BitVec w} (n : Nat) (h : n ∣ a) :
-  x.toInt >>> n = if 2*x.toNat < 2^w then x.toNat >>> n else x.toNat >>> n - 2^n := by
-  simp [toInt_eq_toNat_cond, Int.shiftRight_eq_div_pow]
-  rw [Int.bmod_def]
-  norm_cast
-  split
-  · split
-    · exact?
 
 
-#eval (-19 : Int) >>> 0
-@[simp]
-theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
+-- theorem toInt_shiftRights {x : BitVec w} (n : Nat) (h : n ∣ a) :
+--   x.toInt >>> n = if 2*x.toNat < 2^w then x.toNat >>> n else x.toNat >>> n - 2^n := by
+--   simp [toInt_eq_toNat_cond, Int.shiftRight_eq_div_pow]
+--   rw [Int.bmod_def]
+--   norm_cast
+--   split
+--   · split
+--     · exact?
+
+
+theorem toInt_sshiftRight_of_pos {x : BitVec w} {n : Nat} (hn : 0 < n) :
     (x.sshiftRight n).toInt = x.toInt >>> n := by
     simp only [BitVec.sshiftRight, toInt_ofInt]
     by_cases h : 2 * x.toNat < 2^w
@@ -1836,7 +1839,6 @@ theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
       have h4 : ¬ Int.negSucc a + 2^w < (2^w + 1) /2 := by
         simp only [Int.not_lt, Nat.not_lt] at *
         rw [← ha]
-        have : 2^w/2 ≤ (2^w+1)/2 := sorry
         omega
       rw [Int.emod_def, Int.shiftRight_eq_div_pow]
       push_cast
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 3c471d06ca6a..e3f99a17c731 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -627,6 +627,17 @@ where
   | -[_+1], 0 => Nat.zero_le _
   | -[_+1], succ _ => Nat.succ_le_succ (Nat.div_le_self _ _)
 
+theorem natAbs_div_lt_natAbs_of_pos (a b : Int) (ha : 0 < natAbs a) (hb : 1 < natAbs b) :
+  natAbs (a / b) < natAbs a :=
+  match b, eq_nat_or_neg b with
+  | _, ⟨n, .inl rfl⟩ => aux _ _ _ _
+  | _, ⟨n, .inr rfl⟩ => by simp only [natAbs_neg, Int.ediv_neg] at * ; apply aux <;> assumption
+where
+  aux : ∀ (a : Int) (n : Nat), 0 < natAbs a → 1 < n → natAbs (a / n) < natAbs a
+  | ofNat _, _ => fun h1 h2 => by simp at *; exact Nat.div_lt_self h1 h2
+  | -[_+1], 0 => sorry
+  | -[_+1], succ _ => fun h1 h2 => Nat.succ_le_succ (Nat.div_lt_self _ _ _ )
+
 theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a := by
   have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_div_le_natAbs a b)
   rwa [natAbs_of_nonneg Ha] at this

From 4a775d7b2a3fe9203975e316ba0d437edf3a8b00 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Mon, 9 Dec 2024 16:03:19 -0800
Subject: [PATCH 08/19] thm proved finally

---
 src/Init/Data/BitVec/Lemmas.lean    | 138 +++++++++-------------------
 src/Init/Data/Int/DivModLemmas.lean |  12 ---
 2 files changed, 45 insertions(+), 105 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 01b518104324..15a65cc650c9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -235,12 +235,16 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
 theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp [← getLsbD_eq_getElem]
 
 theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
+theorem toInt_zero_length (x : BitVec 0) : x.toInt = 0 := by simp [of_length_zero]
+
 theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp
 theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by simp
 theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0 := by
   subst h; simp [toNat_zero_length]
+theorem toInt_of_zero_length (h : w = 0) (x : BitVec w) : x.toInt = 0 := by
+  subst h; simp [toInt_zero_length]
 theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false := by
   subst h; simp [getLsbD_zero_length]
 theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false := by
@@ -1758,100 +1762,48 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
     apply BitVec.lt_of_getLsbD hlsb
   · simp [sshiftRight_eq_of_msb_true hmsb]
 
-
-#eval ((6#4).sshiftRight 4).toInt
-#eval ((6#4).toInt >>> 4)
-
-
-
-
-#check Int.emod_def
-#check Int.neg_tdiv
-#check toInt_neg_iff
-
-
-#eval (-7)/16
-
-
-#eval ((9#4).toInt).bmod 16
-#eval (9#4).toInt >>>1
-#eval (-15) % 16
-#eval (-7) % 16
-#check Int.bmod_lt
-#eval (9#4).toInt
-#eval ((10#4) >>>1).toInt
-#eval 8 >>> 0
-
--- when is x % 2^w - 2^w = x for integers x
--- when is x % 2^w = x for integers
-
-#check Int.ediv_eq_zero_of_lt
-#check Int.neg_ofNat_succ
-#check Int.neg_emod
-#check Int.emod_def
-#eval (-3)/5
-#eval -(3/5)
-
-example (a b : Int) (h : b  < 0) (h1 : a ≤ 0): ∃ m, b = Int.negSucc m  := by
-  exact Int.eq_negSucc_of_lt_zero h
-
-#check Nat.div_lt_self
-example ( a b c : Int) : a/b/c = a/(b*c) := sorry
-
-example ( a b c : Int) (h : 0 < b) : (a/b).natAbs < a.natAbs := by
-  push_cast
-  simp only [Int.natAbs_ediv, Int.natAbs_lt_natAbs]
-
-
-
--- theorem toInt_shiftRights {x : BitVec w} (n : Nat) (h : n ∣ a) :
---   x.toInt >>> n = if 2*x.toNat < 2^w then x.toNat >>> n else x.toNat >>> n - 2^n := by
---   simp [toInt_eq_toNat_cond, Int.shiftRight_eq_div_pow]
---   rw [Int.bmod_def]
---   norm_cast
---   split
---   · split
---     · exact?
-
-
-theorem toInt_sshiftRight_of_pos {x : BitVec w} {n : Nat} (hn : 0 < n) :
+theorem toInt_sshiftRight_of_pos {x : BitVec w} {n : Nat} :
     (x.sshiftRight n).toInt = x.toInt >>> n := by
-    simp only [BitVec.sshiftRight, toInt_ofInt]
-    by_cases h : 2 * x.toNat < 2^w
-    · have := Nat.lt_of_le_of_lt (Nat.shiftRight_le x.toNat n) x.isLt
-      have h2 : (x.toNat >>> n) % 2^w < (2^w + 1)/2 := by sorry
-      simp only [toInt_eq_toNat_cond, h, Int.natCast_shiftRight, ite_true]
-      norm_cast
-      simp only [h2, ite_true, Int.ofNat_emod]
-      rw [Int.emod_eq_of_lt (by norm_cast; simp) (by norm_cast)]
-    · have h0 : x.toInt < 0 := by
-        simp only [toInt_eq_toNat_cond, h, ite_false]
-        apply Int.sub_neg_of_lt (by norm_cast; simp [x.isLt])
-      have h1 := Int.ediv_neg' (b := 2^n) h0 (by norm_cast; exact Nat.two_pow_pos n)
-      have ⟨a, ha⟩ := Int.eq_negSucc_of_lt_zero h1
-      have ha1 : a < 2^w := sorry
-      have h2 := Int.ofNat_le.mpr (Int.natAbs_div_le_natAbs x.toInt (2^n))
-      simp only [Int.ofNat_natAbs_of_nonpos _,
-                 Int.le_of_lt h1, Int.le_of_lt h0] at h2
-      have h3 : x.toInt ≥ -2^w/2 := by
-        simp only [toInt_eq_toNat_cond, h, ite_false]
-        norm_cast; omega
-      have h4 : ¬ Int.negSucc a + 2^w < (2^w + 1) /2 := by
-        simp only [Int.not_lt, Nat.not_lt] at *
-        rw [← ha]
-        omega
-      rw [Int.emod_def, Int.shiftRight_eq_div_pow]
-      push_cast
-      rw [ha, Int.negSucc_ediv _ (by norm_cast; exact Nat.two_pow_pos w),
-          ← show ∀ a b, a/b = Int.ediv a b by intros; rfl,
-          Int.ediv_eq_zero_of_lt (by norm_cast; simp) (by norm_cast)]
-      simp [h4]
-
-    -- rw [Int.bmod_eq_of_lt]
-    -- rw [Int.emod_eq_of_lt]
-    -- norm_cast
-    -- rw [Nat.mod_eq_of_lt]
-    -- sorry
+  match w with
+  | 0 => simp [BitVec.sshiftRight, toInt_ofInt, Int.bmod_def, toInt_zero_length]
+  | w + 1 =>
+      simp only [BitVec.sshiftRight, toInt_ofInt, Int.bmod_def]
+      by_cases h : 2 * x.toNat < 2^(w + 1)
+      · have := Nat.lt_of_le_of_lt (Nat.shiftRight_le x.toNat n) x.isLt
+        have h2 : (x.toNat >>> n) % 2^(w + 1) < (2^(w + 1) + 1)/2 := by
+          rw [Nat.mod_eq_of_lt this, Nat.shiftRight_eq_div_pow]
+          apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _)
+          omega
+        simp only [toInt_eq_toNat_cond, h, Int.natCast_shiftRight, ite_true]
+        norm_cast
+        simp only [h2, ite_true, Int.ofNat_emod]
+        rw [Int.emod_eq_of_lt (by norm_cast; simp) (by norm_cast)]
+      · have h0 : x.toInt < 0 := by
+          simp only [toInt_eq_toNat_cond, h, ite_false]
+          apply Int.sub_neg_of_lt (by norm_cast; simp [x.isLt])
+        have h1 := Int.ediv_neg' (b := 2^n) h0 (by norm_cast; exact Nat.two_pow_pos n)
+        have ⟨a, ha⟩ := Int.eq_negSucc_of_lt_zero h1
+        have h2 := Int.ofNat_le.mpr (Int.natAbs_div_le_natAbs x.toInt (2^n))
+        simp only [Int.ofNat_natAbs_of_nonpos _,
+                  Int.le_of_lt h1, Int.le_of_lt h0] at h2
+        have h3 : x.toInt ≥ -2^(w + 1)/2 := by
+          simp only [toInt_eq_toNat_cond, h, ite_false]
+          norm_cast; omega
+        have ha1 : a < 2^(w + 1):= by
+          simp only [← Int.ofNat_lt, Int.negSucc_eq'] at *
+          rw [show a = -(x.toInt / 2^n) - 1 by omega]
+          push_cast; omega
+        have h4 : ¬ Int.negSucc a + 2^(w + 1) < (2^(w + 1) + 1) /2 := by
+          simp only [Int.not_lt, Nat.not_lt] at *; norm_cast
+          rw [Nat.pow_succ, Nat.mul_comm, Nat.mul_add_div, ← ha]
+          push_cast
+          omega; decide
+        rw [Int.emod_def, Int.shiftRight_eq_div_pow]
+        push_cast
+        rw [ha, Int.negSucc_ediv _ (by norm_cast; exact Nat.two_pow_pos _),
+            ← show ∀ a b, a/b = Int.ediv a b by intros; rfl,
+            Int.ediv_eq_zero_of_lt (by norm_cast; simp) (by norm_cast)]
+        simp [h4]
 
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index e3f99a17c731..f9ddf51c15c6 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -626,18 +626,6 @@ where
   | ofNat _, _ => Nat.div_le_self ..
   | -[_+1], 0 => Nat.zero_le _
   | -[_+1], succ _ => Nat.succ_le_succ (Nat.div_le_self _ _)
-
-theorem natAbs_div_lt_natAbs_of_pos (a b : Int) (ha : 0 < natAbs a) (hb : 1 < natAbs b) :
-  natAbs (a / b) < natAbs a :=
-  match b, eq_nat_or_neg b with
-  | _, ⟨n, .inl rfl⟩ => aux _ _ _ _
-  | _, ⟨n, .inr rfl⟩ => by simp only [natAbs_neg, Int.ediv_neg] at * ; apply aux <;> assumption
-where
-  aux : ∀ (a : Int) (n : Nat), 0 < natAbs a → 1 < n → natAbs (a / n) < natAbs a
-  | ofNat _, _ => fun h1 h2 => by simp at *; exact Nat.div_lt_self h1 h2
-  | -[_+1], 0 => sorry
-  | -[_+1], succ _ => fun h1 h2 => Nat.succ_le_succ (Nat.div_lt_self _ _ _ )
-
 theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a := by
   have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_div_le_natAbs a b)
   rwa [natAbs_of_nonneg Ha] at this

From 5c3d2decc36c8c9e5c23346f70a7c1239106be7a Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Mon, 9 Dec 2024 16:03:40 -0800
Subject: [PATCH 09/19] small change

---
 src/Init/Data/Int/DivModLemmas.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index f9ddf51c15c6..3c471d06ca6a 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -626,6 +626,7 @@ where
   | ofNat _, _ => Nat.div_le_self ..
   | -[_+1], 0 => Nat.zero_le _
   | -[_+1], succ _ => Nat.succ_le_succ (Nat.div_le_self _ _)
+
 theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a := by
   have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_div_le_natAbs a b)
   rwa [natAbs_of_nonneg Ha] at this

From 9b5ad73c5f54a4e8d96cb0e55e68e136fc567c81 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Mon, 9 Dec 2024 16:10:56 -0800
Subject: [PATCH 10/19] small change

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 15a65cc650c9..a76d26e4e926 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1762,7 +1762,7 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
     apply BitVec.lt_of_getLsbD hlsb
   · simp [sshiftRight_eq_of_msb_true hmsb]
 
-theorem toInt_sshiftRight_of_pos {x : BitVec w} {n : Nat} :
+theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
     (x.sshiftRight n).toInt = x.toInt >>> n := by
   match w with
   | 0 => simp [BitVec.sshiftRight, toInt_ofInt, Int.bmod_def, toInt_zero_length]

From 2db7a2527e1a34f7e866ad5b7e83736d7b37ffcd Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Mon, 9 Dec 2024 16:17:33 -0800
Subject: [PATCH 11/19] extra stuff

---
 src/Init/Data/Int/DivModLemmas.lean | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 3c471d06ca6a..40471b86c2dd 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -550,23 +550,6 @@ theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
   match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
 
--- #check Int.ediv_eq_zero_of_lt
--- #eval (-3)/10
--- #eval (-3)%10
-
--- theorem emod_eq_of_gt_lt {a b : Int} (H1 : -b < a) (H2 : a < b) : a % b = a := by
---   rw [Int.emod_def]
---   have : a/b = 0 := by
---     simp [Int.ediv_]
---   rw [natAbs_eq_zero] at this
---   simp [this]
-
-
-
-
-  -- match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
-  -- | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
-
 @[simp] theorem emod_self_add_one {x : Int} (h : 0 ≤ x) : x % (x + 1) = x :=
   emod_eq_of_lt h (Int.lt_succ x)
 

From dd214afbc3408f022e5b3ea1594b9c94f9f3a45a Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sun, 16 Feb 2025 19:13:51 +0000
Subject: [PATCH 12/19] make it work

---
 src/Init/Data/BitVec/Lemmas.lean      | 179 +++++++++++++++++---------
 src/Init/Data/Int/Bitwise/Lemmas.lean |  28 ++++
 src/Init/Data/Int/DivModLemmas.lean   |   3 +
 src/Init/Data/Int/LemmasAux.lean      |   7 +
 4 files changed, 157 insertions(+), 60 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a76d26e4e926..6f4c7c617f17 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -14,6 +14,7 @@ import Init.Data.Nat.Mod
 import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.Pow
+import Init.Data.Int.LemmasAux
 
 set_option linter.missingDocs true
 
@@ -586,23 +587,6 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
     0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
   simp [toInt_eq_toNat_cond]; omega
 
-theorem toInt_lt {w : Nat} {x : BitVec w} : BitVec.toInt x < 2^w := by
-  simp only [toInt_eq_toNat_cond]
-  split
-  · norm_cast; simp [x.isLt]
-  · apply Int.lt_trans (Int.sub_lt_self _ (by norm_cast; apply Nat.two_pow_pos w))
-                       (by norm_cast; exact x.isLt)
-
-theorem toInt_gt {w : Nat} {x : BitVec w} : -2^w < BitVec.toInt x := by
-  simp only [toInt_eq_toNat_cond]
-  split
-  · apply Int.lt_of_lt_of_le (by apply Int.neg_neg_of_pos; norm_cast; exact Nat.two_pow_pos w)
-                             (by norm_cast; simp)
-  · norm_cast
-    rw [Int.sub_eq_add_neg]
-    apply Int.lt_add_of_pos_left
-    omega
-
 theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
   obtain ⟨a, ha⟩ := a
   simp only [Nat.reducePow]
@@ -629,6 +613,14 @@ theorem toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
+theorem toInt_lt' {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by
+  by_cases h : w = 0
+  · subst h
+    simp [eq_nil x]
+  · have := @toInt_lt w x
+    rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this
+    omega
+
 /--
 `x.toInt` is greater than or equal to `-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.
@@ -641,6 +633,14 @@ theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
+theorem le_toInt' {w : Nat} {x : BitVec w} : -2 ^ (w - 1) ≤ x.toInt := by
+  by_cases h : w = 0
+  · subst h
+    simp [eq_nil x]
+  · have := @le_toInt w x
+    rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this
+    omega
+
 /-! ### slt -/
 
 /--
@@ -1762,49 +1762,6 @@ theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
     apply BitVec.lt_of_getLsbD hlsb
   · simp [sshiftRight_eq_of_msb_true hmsb]
 
-theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
-    (x.sshiftRight n).toInt = x.toInt >>> n := by
-  match w with
-  | 0 => simp [BitVec.sshiftRight, toInt_ofInt, Int.bmod_def, toInt_zero_length]
-  | w + 1 =>
-      simp only [BitVec.sshiftRight, toInt_ofInt, Int.bmod_def]
-      by_cases h : 2 * x.toNat < 2^(w + 1)
-      · have := Nat.lt_of_le_of_lt (Nat.shiftRight_le x.toNat n) x.isLt
-        have h2 : (x.toNat >>> n) % 2^(w + 1) < (2^(w + 1) + 1)/2 := by
-          rw [Nat.mod_eq_of_lt this, Nat.shiftRight_eq_div_pow]
-          apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _)
-          omega
-        simp only [toInt_eq_toNat_cond, h, Int.natCast_shiftRight, ite_true]
-        norm_cast
-        simp only [h2, ite_true, Int.ofNat_emod]
-        rw [Int.emod_eq_of_lt (by norm_cast; simp) (by norm_cast)]
-      · have h0 : x.toInt < 0 := by
-          simp only [toInt_eq_toNat_cond, h, ite_false]
-          apply Int.sub_neg_of_lt (by norm_cast; simp [x.isLt])
-        have h1 := Int.ediv_neg' (b := 2^n) h0 (by norm_cast; exact Nat.two_pow_pos n)
-        have ⟨a, ha⟩ := Int.eq_negSucc_of_lt_zero h1
-        have h2 := Int.ofNat_le.mpr (Int.natAbs_div_le_natAbs x.toInt (2^n))
-        simp only [Int.ofNat_natAbs_of_nonpos _,
-                  Int.le_of_lt h1, Int.le_of_lt h0] at h2
-        have h3 : x.toInt ≥ -2^(w + 1)/2 := by
-          simp only [toInt_eq_toNat_cond, h, ite_false]
-          norm_cast; omega
-        have ha1 : a < 2^(w + 1):= by
-          simp only [← Int.ofNat_lt, Int.negSucc_eq'] at *
-          rw [show a = -(x.toInt / 2^n) - 1 by omega]
-          push_cast; omega
-        have h4 : ¬ Int.negSucc a + 2^(w + 1) < (2^(w + 1) + 1) /2 := by
-          simp only [Int.not_lt, Nat.not_lt] at *; norm_cast
-          rw [Nat.pow_succ, Nat.mul_comm, Nat.mul_add_div, ← ha]
-          push_cast
-          omega; decide
-        rw [Int.emod_def, Int.shiftRight_eq_div_pow]
-        push_cast
-        rw [ha, Int.negSucc_ediv _ (by norm_cast; exact Nat.two_pow_pos _),
-            ← show ∀ a b, a/b = Int.ediv a b by intros; rfl,
-            Int.ediv_eq_zero_of_lt (by norm_cast; simp) (by norm_cast)]
-        simp [h4]
-
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
   ext i
@@ -1897,6 +1854,108 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
         by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)
   · simp [h]
 
+theorem toInt_le_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt ≤ 0 := by
+  simp only [BitVec.toInt]
+  have : 2 * x.toNat ≥ 2 ^ w := msb_eq_true_iff_two_mul_ge.mp h
+  omega
+
+theorem le_toInt_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.toInt := by
+  simp only [BitVec.toInt]
+  have : 2 * x.toNat < 2 ^ w := msb_eq_false_iff_two_mul_lt.mp h
+  omega
+
+theorem le_shiftRight_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s := by
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  split
+  case _ _ _ m =>
+    simp
+    simp [Int.ofNat_eq_coe] at h
+    by_cases hm : m = 0
+    · simp [hm]
+    · omega
+  case _ _ _ m =>
+    by_cases hm : m = 0
+    · simp [hm]
+    · have := Nat.shiftRight_le m s
+      omega
+
+theorem shiftRight_le_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n := by
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  split
+  case _ _ _ m =>
+    simp only [Int.ofNat_eq_coe] at h
+    by_cases hm : m = 0
+    · simp [hm]
+    · have := Nat.shiftRight_le m s
+      simp
+      omega
+  case _ _ _ m =>
+    omega
+
+theorem le_shiftRight_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : 0 ≤ (n >>> s) := by
+  rw [Int.shiftRight_eq_div_pow]
+  by_cases h' : s = 0
+  · simp [h', h]
+  · have rl :=  @Int.le_ediv_of_mul_le 0 n (2^s) (by
+      have := @Nat.one_lt_two_pow s (by omega)
+      norm_cast at *
+      omega
+    )
+    simp at rl
+    have rt := rl h
+    norm_cast at *
+
+theorem shiftRight_le_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : (n >>> s) ≤ 0 := by
+  rw [Int.shiftRight_eq_div_pow]
+  by_cases h' : s = 0
+  · simp [h', h]
+  · have rl := @Int.ediv_le_of_le_mul n 0 (2^s) (by
+      have := @Nat.one_lt_two_pow s (by omega)
+      norm_cast at *
+      omega
+    )
+    simp at rl
+    have rt := rl h
+    norm_cast at *
+
+theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
+    (x.sshiftRight n).toInt = x.toInt >>> n := by
+  by_cases h : w = 0
+  · subst h
+    simp [BitVec.eq_nil x]
+  · simp only [sshiftRight, toInt_ofInt]
+    have h1 : -↑((2 ^ w) : Nat) ≤ x.toInt >>> n * 2 := by
+      rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.mul_two]
+      push_cast
+      rw [←Int.neg_mul]
+      by_cases hh : x.toInt ≤ 0
+      · have aa : -2 ^ (w - 1) ≤ x.toInt >>> n := by
+          have := @BitVec.le_toInt' w x
+          have := Int.le_shiftRight_of_le x.toInt n
+          omega
+        exact Int.mul_le_mul_of_nonneg_right aa (by decide)
+      · have : 0 ≤ x.toInt >>> n := le_shiftRight_of_nonneg x.toInt n (by omega)
+        simp
+        norm_cast
+        omega
+    have h2 : x.toInt >>> n * 2 < ↑((2 ^ w) : Nat) := by
+      rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.mul_two]
+      push_cast
+      by_cases hh : x.toInt ≤ 0
+      · have : x.toInt >>> n ≤ 0  := shiftRight_le_of_nonpos x.toInt n (by omega)
+        have : 2 ^ (w - 1) * 2 > 0 := by
+          have := @Nat.one_le_two_pow (w - 1)
+          omega
+        simp
+        norm_cast
+        omega
+      · have aa : x.toInt >>> n < 2 ^ (w - 1) := by
+          have := @BitVec.toInt_lt' w x
+          have := shiftRight_le_of_nonneg x.toInt n
+          omega
+        exact Int.mul_lt_mul_of_pos_right aa (by decide)
+    exact Int.bmod_eq_of_le_of_lt h1 h2
+
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
 @[simp]
diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean
index 9b7b41597a88..bf27656bf09b 100644
--- a/src/Init/Data/Int/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Int/Bitwise/Lemmas.lean
@@ -38,4 +38,32 @@ theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
 theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
+theorem le_shiftRight_of_le (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s := by
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  split
+  case _ _ _ m =>
+    simp
+    simp [Int.ofNat_eq_coe] at h
+    by_cases hm : m = 0
+    · simp [hm]
+    · omega
+  case _ _ _ m =>
+    by_cases hm : m = 0
+    · simp [hm]
+    · have := Nat.shiftRight_le m s
+      omega
+
+theorem shiftRight_le_of_le (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n := by
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  split
+  case _ _ _ m =>
+    simp only [Int.ofNat_eq_coe] at h
+    by_cases hm : m = 0
+    · simp [hm]
+    · have := Nat.shiftRight_le m s
+      simp
+      omega
+  case _ _ _ m =>
+    omega
+
 end Int
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 40471b86c2dd..1e0fccfd68fe 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -484,6 +484,9 @@ theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
 theorem neg_emod {a b : Int} : -a % b = (b - a) % b := by
   rw [← add_emod_self_left]; rfl
 
+theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b :=
+  Int.add_emod_self.symm
+
 @[simp] theorem emod_neg (a b : Int) : a % -b = a % b := by
   rw [emod_def, emod_def, Int.ediv_neg, Int.neg_mul_neg]
 
diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean
index 756b1cc6676e..ccf56260f5d6 100644
--- a/src/Init/Data/Int/LemmasAux.lean
+++ b/src/Init/Data/Int/LemmasAux.lean
@@ -45,4 +45,11 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) :
   · rw [Int.emod_eq_of_lt xpos (by omega)]; omega
   · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega
 
+theorem bmod_eq_of_le_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) :
+    x.bmod y = x := by
+  simp only [Int.bmod_def]
+  rcases x
+  · rw [Int.emod_eq_of_lt (by simp only [ofNat_eq_coe]; omega) (by omega)]; omega
+  · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega
+
 end Int

From 222bfc4f3dedae27212ec4c006a009c11d25a256 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sun, 16 Feb 2025 19:14:34 +0000
Subject: [PATCH 13/19] make it work

---
 src/Init/Data/BitVec/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 6f4c7c617f17..fffd87f25ba1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1925,7 +1925,7 @@ theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
     simp [BitVec.eq_nil x]
   · simp only [sshiftRight, toInt_ofInt]
     have h1 : -↑((2 ^ w) : Nat) ≤ x.toInt >>> n * 2 := by
-      rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.mul_two]
+      rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.mul_two]
       push_cast
       rw [←Int.neg_mul]
       by_cases hh : x.toInt ≤ 0
@@ -1939,7 +1939,7 @@ theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
         norm_cast
         omega
     have h2 : x.toInt >>> n * 2 < ↑((2 ^ w) : Nat) := by
-      rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.mul_two]
+      rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.mul_two]
       push_cast
       by_cases hh : x.toInt ≤ 0
       · have : x.toInt >>> n ≤ 0  := shiftRight_le_of_nonpos x.toInt n (by omega)

From dfac93d79ed55247aad0ce02b05fee999f03208d Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sun, 16 Feb 2025 20:39:48 +0000
Subject: [PATCH 14/19] restructure proof

---
 src/Init/Data/BitVec/Lemmas.lean | 56 ++++++++++++++------------------
 1 file changed, 24 insertions(+), 32 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index fffd87f25ba1..e34a81fc3fe6 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1918,43 +1918,35 @@ theorem shiftRight_le_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : (n >>> s) 
     have rt := rl h
     norm_cast at *
 
+theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} :
+    x.toInt >>> n < 2 ^ (w - 1) := by
+  have := shiftRight_le_of_nonneg x.toInt n
+  have := @BitVec.toInt_lt' w x
+  have := shiftRight_le_of_nonpos x.toInt n
+  have := @Nat.one_le_two_pow (w-1)
+  norm_cast at *
+  omega
+
+theorem lt_toInt_shiftRight {x : BitVec w} {n : Nat} :
+    -(2 ^ (w - 1)) ≤ x.toInt >>> n := by
+  have := le_shiftRight_of_nonpos x.toInt n
+  have := le_shiftRight_of_nonneg x.toInt n
+  have := @Nat.one_le_two_pow (w-1)
+  have := @BitVec.le_toInt' w x
+  norm_cast at *
+  omega
+
+@[simp]
 theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
     (x.sshiftRight n).toInt = x.toInt >>> n := by
   by_cases h : w = 0
   · subst h
     simp [BitVec.eq_nil x]
-  · simp only [sshiftRight, toInt_ofInt]
-    have h1 : -↑((2 ^ w) : Nat) ≤ x.toInt >>> n * 2 := by
-      rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.mul_two]
-      push_cast
-      rw [←Int.neg_mul]
-      by_cases hh : x.toInt ≤ 0
-      · have aa : -2 ^ (w - 1) ≤ x.toInt >>> n := by
-          have := @BitVec.le_toInt' w x
-          have := Int.le_shiftRight_of_le x.toInt n
-          omega
-        exact Int.mul_le_mul_of_nonneg_right aa (by decide)
-      · have : 0 ≤ x.toInt >>> n := le_shiftRight_of_nonneg x.toInt n (by omega)
-        simp
-        norm_cast
-        omega
-    have h2 : x.toInt >>> n * 2 < ↑((2 ^ w) : Nat) := by
-      rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.mul_two]
-      push_cast
-      by_cases hh : x.toInt ≤ 0
-      · have : x.toInt >>> n ≤ 0  := shiftRight_le_of_nonpos x.toInt n (by omega)
-        have : 2 ^ (w - 1) * 2 > 0 := by
-          have := @Nat.one_le_two_pow (w - 1)
-          omega
-        simp
-        norm_cast
-        omega
-      · have aa : x.toInt >>> n < 2 ^ (w - 1) := by
-          have := @BitVec.toInt_lt' w x
-          have := shiftRight_le_of_nonneg x.toInt n
-          omega
-        exact Int.mul_lt_mul_of_pos_right aa (by decide)
-    exact Int.bmod_eq_of_le_of_lt h1 h2
+  · rw [sshiftRight, toInt_ofInt, ←Nat.two_pow_pred_add_two_pow_pred (by omega)]
+    have := @toInt_shiftRight_lt w x n
+    have := @lt_toInt_shiftRight w x n
+    norm_cast at *
+    exact Int.bmod_eq_of_le_of_lt (by omega) (by omega)
 
 /-! ### sshiftRight reductions from BitVec to Nat -/
 

From 8c5746412c1abf511b881c45cd1f3cdd79bcdcfb Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 17 Feb 2025 00:18:12 +0000
Subject: [PATCH 15/19] restructure proof

---
 src/Init/Data/BitVec/Lemmas.lean | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e34a81fc3fe6..d0efa46a74f1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1892,30 +1892,23 @@ theorem shiftRight_le_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤
   case _ _ _ m =>
     omega
 
+theorem ediv_neg_of_neg_of_pos (n s : Int) (h : n ≤ 0) (h2 : 0 < s) : n / s ≤ 0 :=
+  Int.ediv_le_of_le_mul (by omega) (by omega)
+
 theorem le_shiftRight_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : 0 ≤ (n >>> s) := by
   rw [Int.shiftRight_eq_div_pow]
   by_cases h' : s = 0
   · simp [h', h]
-  · have rl :=  @Int.le_ediv_of_mul_le 0 n (2^s) (by
-      have := @Nat.one_lt_two_pow s (by omega)
-      norm_cast at *
-      omega
-    )
-    simp at rl
-    have rt := rl h
+  · have := @Nat.pow_pos 2 s (by omega)
+    have := @Int.ediv_nonneg n (2^s) h (by norm_cast at *; omega)
     norm_cast at *
 
 theorem shiftRight_le_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : (n >>> s) ≤ 0 := by
   rw [Int.shiftRight_eq_div_pow]
   by_cases h' : s = 0
   · simp [h', h]
-  · have rl := @Int.ediv_le_of_le_mul n 0 (2^s) (by
-      have := @Nat.one_lt_two_pow s (by omega)
-      norm_cast at *
-      omega
-    )
-    simp at rl
-    have rt := rl h
+  · have : 1 < 2 ^ s := Nat.one_lt_two_pow (by omega)
+    have rl : n / 2 ^ s ≤ 0 := ediv_neg_of_neg_of_pos n (2^s) (by omega) (by norm_cast at *; omega)
     norm_cast at *
 
 theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} :

From dbd31e0be91ecf9f4dffe3fd37a07cb166d1bc7b Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 17 Feb 2025 00:30:59 +0000
Subject: [PATCH 16/19] WIP

---
 src/Init/Data/BitVec/Lemmas.lean      | 57 +++------------------------
 src/Init/Data/Int/Bitwise/Lemmas.lean | 20 +++++++++-
 src/Init/Data/Int/DivModLemmas.lean   | 17 +++++++-
 src/Init/Data/Int/Lemmas.lean         |  1 +
 4 files changed, 39 insertions(+), 56 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index d0efa46a74f1..e1b7fe75075b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1864,68 +1864,21 @@ theorem le_toInt_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.toInt
   have : 2 * x.toNat < 2 ^ w := msb_eq_false_iff_two_mul_lt.mp h
   omega
 
-theorem le_shiftRight_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s := by
-  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
-  split
-  case _ _ _ m =>
-    simp
-    simp [Int.ofNat_eq_coe] at h
-    by_cases hm : m = 0
-    · simp [hm]
-    · omega
-  case _ _ _ m =>
-    by_cases hm : m = 0
-    · simp [hm]
-    · have := Nat.shiftRight_le m s
-      omega
-
-theorem shiftRight_le_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n := by
-  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
-  split
-  case _ _ _ m =>
-    simp only [Int.ofNat_eq_coe] at h
-    by_cases hm : m = 0
-    · simp [hm]
-    · have := Nat.shiftRight_le m s
-      simp
-      omega
-  case _ _ _ m =>
-    omega
-
-theorem ediv_neg_of_neg_of_pos (n s : Int) (h : n ≤ 0) (h2 : 0 < s) : n / s ≤ 0 :=
-  Int.ediv_le_of_le_mul (by omega) (by omega)
-
-theorem le_shiftRight_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : 0 ≤ (n >>> s) := by
-  rw [Int.shiftRight_eq_div_pow]
-  by_cases h' : s = 0
-  · simp [h', h]
-  · have := @Nat.pow_pos 2 s (by omega)
-    have := @Int.ediv_nonneg n (2^s) h (by norm_cast at *; omega)
-    norm_cast at *
-
-theorem shiftRight_le_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : (n >>> s) ≤ 0 := by
-  rw [Int.shiftRight_eq_div_pow]
-  by_cases h' : s = 0
-  · simp [h', h]
-  · have : 1 < 2 ^ s := Nat.one_lt_two_pow (by omega)
-    have rl : n / 2 ^ s ≤ 0 := ediv_neg_of_neg_of_pos n (2^s) (by omega) (by norm_cast at *; omega)
-    norm_cast at *
-
 theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} :
     x.toInt >>> n < 2 ^ (w - 1) := by
-  have := shiftRight_le_of_nonneg x.toInt n
+  have := Int.shiftRight_le_of_nonneg x.toInt n
+  have := Int.shiftRight_le_of_nonpos x.toInt n
   have := @BitVec.toInt_lt' w x
-  have := shiftRight_le_of_nonpos x.toInt n
   have := @Nat.one_le_two_pow (w-1)
   norm_cast at *
   omega
 
 theorem lt_toInt_shiftRight {x : BitVec w} {n : Nat} :
     -(2 ^ (w - 1)) ≤ x.toInt >>> n := by
-  have := le_shiftRight_of_nonpos x.toInt n
-  have := le_shiftRight_of_nonneg x.toInt n
-  have := @Nat.one_le_two_pow (w-1)
+  have := Int.le_shiftRight_of_nonpos x.toInt n
+  have := Int.le_shiftRight_of_nonneg x.toInt n
   have := @BitVec.le_toInt' w x
+  have := @Nat.one_le_two_pow (w-1)
   norm_cast at *
   omega
 
diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean
index bf27656bf09b..efb7888e024a 100644
--- a/src/Init/Data/Int/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Int/Bitwise/Lemmas.lean
@@ -38,7 +38,7 @@ theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
 theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
-theorem le_shiftRight_of_le (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s := by
+theorem le_shiftRight_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s := by
   simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
   split
   case _ _ _ m =>
@@ -53,7 +53,7 @@ theorem le_shiftRight_of_le (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s :=
     · have := Nat.shiftRight_le m s
       omega
 
-theorem shiftRight_le_of_le (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n := by
+theorem shiftRight_le_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n := by
   simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
   split
   case _ _ _ m =>
@@ -66,4 +66,20 @@ theorem shiftRight_le_of_le (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n :=
   case _ _ _ m =>
     omega
 
+theorem le_shiftRight_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : 0 ≤ (n >>> s) := by
+  rw [Int.shiftRight_eq_div_pow]
+  by_cases h' : s = 0
+  · simp [h', h]
+  · have := @Nat.pow_pos 2 s (by omega)
+    have := @Int.ediv_nonneg n (2^s) h (by norm_cast at *; omega)
+    norm_cast at *
+
+theorem shiftRight_le_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : (n >>> s) ≤ 0 := by
+  rw [Int.shiftRight_eq_div_pow]
+  by_cases h' : s = 0
+  · simp [h', h]
+  · have : 1 < 2 ^ s := Nat.one_lt_two_pow (by omega)
+    have rl : n / 2 ^ s ≤ 0 := Int.ediv_neg_of_neg_of_pos (by omega) (by norm_cast at *; omega)
+    norm_cast at *
+
 end Int
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 1e0fccfd68fe..aaa57d992d0e 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -287,10 +287,20 @@ theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod
 
 /-! ### `/` ediv -/
 
+#check Int.ediv
+
 @[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
-  | ofNat _, -[_+1] => (Int.neg_neg _).symm
-  | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
+  | ofNat _, -[_+1] => show ofNat _ / - -[_+1] = -(ofNat _ / -[_+1]) by
+    rename_i a b
+    have ar : ofNat a / - -[b+1] = -(ofNat a / -[b+1]) := by
+      have as := @Int.neg_neg
+      exact (as _).symm
+    exact ar
+  | ofNat _, succ _ => rfl
+  | -[_+1], 0 => rfl
+  | -[_+1], succ _ => rfl
+  | -[_+1], -[_+1] => rfl
 
 theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
   match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
@@ -763,6 +773,9 @@ theorem le_of_mul_le_mul_right {a b c : Int} (w : b * a ≤ c * a) (h : 0 < a) :
 protected theorem ediv_le_of_le_mul {a b c : Int} (H : 0 < c) (H' : a ≤ b * c) : a / c ≤ b :=
   le_of_mul_le_mul_right (Int.le_trans (Int.ediv_mul_le _ (Int.ne_of_gt H)) H') H
 
+protected theorem ediv_neg_of_neg_of_pos {n s : Int} (h : n ≤ 0) (h2 : 0 < s) : n / s ≤ 0 :=
+  Int.ediv_le_of_le_mul h2 (by simp [h])
+
 protected theorem mul_lt_of_lt_ediv {a b c : Int} (H : 0 < c) (H3 : a < b / c) : a * c < b :=
   Int.lt_of_not_ge <| mt (Int.ediv_le_of_le_mul H) (Int.not_le_of_gt H3)
 
diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index 42d8d86e7507..f04168e295b3 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -388,6 +388,7 @@ protected theorem mul_right_comm (a b c : Int) : a * b * c = a * c * b := by
 
 @[simp] protected theorem zero_mul (a : Int) : 0 * a = 0 := Int.mul_comm .. ▸ a.mul_zero
 
+
 theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n := by cases n <;> rfl
 
 theorem ofNat_mul_subNatNat (m n k : Nat) :

From 6c1b916a56a710df1247ee7c651794202bd10427 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 17 Feb 2025 00:31:54 +0000
Subject: [PATCH 17/19] WIP

---
 src/Init/Data/Int/DivModLemmas.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index aaa57d992d0e..5c5beababa7d 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -287,8 +287,6 @@ theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod
 
 /-! ### `/` ediv -/
 
-#check Int.ediv
-
 @[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat _, -[_+1] => show ofNat _ / - -[_+1] = -(ofNat _ / -[_+1]) by

From 9798c8279cc549b569377a6c64df0594710c516e Mon Sep 17 00:00:00 2001
From: Tobias Grosser <github@grosser.es>
Date: Mon, 17 Feb 2025 00:32:23 +0000
Subject: [PATCH 18/19] Update src/Init/Data/Int/Lemmas.lean

---
 src/Init/Data/Int/Lemmas.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index f04168e295b3..42d8d86e7507 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -388,7 +388,6 @@ protected theorem mul_right_comm (a b c : Int) : a * b * c = a * c * b := by
 
 @[simp] protected theorem zero_mul (a : Int) : 0 * a = 0 := Int.mul_comm .. ▸ a.mul_zero
 
-
 theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n := by cases n <;> rfl
 
 theorem ofNat_mul_subNatNat (m n k : Nat) :

From e4353a7562547ca0155cb6e5669c3089a9b7284f Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 17 Feb 2025 00:33:13 +0000
Subject: [PATCH 19/19] WIP

---
 src/Init/Data/Int/DivModLemmas.lean | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 5c5beababa7d..07260d98ead5 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -289,16 +289,8 @@ theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod
 
 @[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
-  | ofNat _, -[_+1] => show ofNat _ / - -[_+1] = -(ofNat _ / -[_+1]) by
-    rename_i a b
-    have ar : ofNat a / - -[b+1] = -(ofNat a / -[b+1]) := by
-      have as := @Int.neg_neg
-      exact (as _).symm
-    exact ar
-  | ofNat _, succ _ => rfl
-  | -[_+1], 0 => rfl
-  | -[_+1], succ _ => rfl
-  | -[_+1], -[_+1] => rfl
+  | ofNat _, -[_+1] => (Int.neg_neg _).symm
+  | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
 
 theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
   match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with