From 52c618d980a81a896cc731411ecb851f447e58a0 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 3 Jun 2024 10:28:40 +0100
Subject: [PATCH] Test

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 6ebe61d3b30b..91f113e80cb8 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -812,15 +812,13 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
       have rr : ¬ (2 * x.toNat < 2 ^ n) := by omega
       simp [rr]
       norm_cast
-      rw [←Int.ofNat_sub]
-      norm_cast
-      rw [Nat.mod_eq_of_lt]
-      · sorry
-      · have ww :=  Nat.pow_lt_pow_of_lt (a := 2) (by omega) xx
-        omega
-      · have ee := BitVec.toNat_lt x
-        simp [ee]
-        sorry
+      unfold instHMod
+      simp_all
+      unfold Mod.mod
+      unfold Int.instMod
+      unfold Int.emod
+      simp
+      -- here the negSucc comes in
     · simp at rr
       simp [rr]
       have tt := BitVec.toNat_lt_of_msb_false rr