wip

src/Init/Data/BitVec/Lemmas.lean

@@ -815,8 +815,15 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
       omega
       sorry
     · simp at rr
+      simp [rr]
       have tt := BitVec.toNat_lt_of_msb_false rr
-      have rr : 2 * x.toNat < 2 ^ n := by sorry
+      have rr : 2 * x.toNat < 2 ^ n := by
+        have ss : 2 ^n = 2 ^(n - 1 + 1) := by
+          rw [Nat.sub_add_cancel]
+          omega
+        rw [ss]
+        rw [Nat.pow_succ]
+        omega
       simp [rr]
       norm_cast
 
@@ -825,6 +832,7 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
 
 
 
+
 /-- To sign extend when the msb is false, then sign extension is the same as truncation -/
 theorem signExtend_eq_neg_truncate_neg_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     (x.signExtend v) = x.zeroExtend v := by