diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
index 1730498d..0bcc4ff1 100644
--- a/Arm/BitVec.lean
+++ b/Arm/BitVec.lean
@@ -378,7 +378,9 @@ theorem nat_bitvec_add (x y : BitVec n) :
   (x + y).toNat = (x.toNat + y.toNat) % 2 ^ n := rfl
 
 theorem nat_bitvec_sub (x y : BitVec n) :
-  (x - y).toNat = (x.toNat + (2^n - y.toNat)) % 2^n := rfl
+  (x - y).toNat = (x.toNat + (2^n - y.toNat)) % 2^n := by
+  have : (x - y).toNat = ((2^n - y.toNat) + x.toNat) % 2^n := rfl
+  rw [this, Nat.add_comm]
 
 ---------------------------- Comparison Lemmas -----------------------
 
@@ -405,7 +407,7 @@ protected theorem val_bitvec_le {n : Nat} {a b : BitVec n} : a.toNat ≤ b.toNat
   Iff.rfl
 
 protected theorem val_nat_le (x y n : Nat)
-  (h0 : x <= y) (h1 : x < 2^n) (h2 : y < 2^n) : 
+  (h0 : x <= y) (h1 : x < 2^n) (h2 : y < 2^n) :
   BitVec.ofNat n x <= BitVec.ofNat n y := by
   rw [BitVec.le_iff_val_le_val]
   simp [bitvec_to_nat_of_nat]
@@ -612,7 +614,7 @@ theorem leftshift_n_or_mod_2n :
 @[bitvec_rules]
 protected theorem truncate_to_lsb_of_append (m n : Nat) (x : BitVec m) (y : BitVec n) :
   truncate n (x ++ y) = y := by
-  simp only [truncate_append, Nat.le_refl, ↓reduceDite, zeroExtend_eq]
+  simp only [truncate_append, Nat.le_refl, ↓reduceDIte, zeroExtend_eq]
 
 ----------------------------------------------------------------------
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 098ea685..32fd0650 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "6141f00e9b5a0b1c92ce971d99082f70345cc6c3",
+   "rev": "686e90d51cd34c619739e9df73bc0bc81972aac6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover/leansat",
    "type": "git",
    "subDir": null,
-   "rev": "02cffbd5bf87042e7cee98e51c5a07f917fc5333",
+   "rev": "4f74ea6a51b0887302eb438c4929c06120041890",
    "name": "LeanSAT",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index d8c33b36..f2fba0bb 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-06-09
+leanprover/lean4:nightly-2024-06-26