toNat

src/Init/Data/BitVec/Lemmas.lean

@@ -1532,10 +1532,6 @@ theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
 theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
   rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
 
-example (a b : Nat) (h : a ≤ b) : ∃ k : Nat, b = a + k:= by
-  exact Nat.exists_eq_add_of_le h
-
-
 theorem toNat_signExtend_of_gt (x : BitVec w) {v : Nat} :
   (x.signExtend (w + v)).toNat = x.toNat + (2 ^ (w + v)  - 2^w) * (if x.msb then 1 else 0) := by
   apply Nat.eq_of_testBit_eq
@@ -1555,8 +1551,9 @@ theorem toNat_signExtend (x : BitVec w) {v : Nat} :
   · rw [signExtend_eq_setWidth_of_lt _ h, toNat_setWidth]
     simp [Nat.sub_eq_zero_of_le (Nat.pow_le_pow_of_le_right Nat.two_pos h)]
   · have ⟨k, hk⟩ := Nat.exists_eq_add_of_le (Nat.le_of_lt (Nat.lt_of_not_le h))
+    have H := Nat.pow_le_pow_of_le_right Nat.two_pos (Nat.le_add_right w k)
     rw [hk, toNat_signExtend_of_gt, toNat_setWidth]
-    rw [Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt ((Nat.pow_le_pow_of_le_right Nat.two_pos (by simp))))]
+    rw [Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
 
 
 /-! ### append -/