diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 09bb88b77e..9defbee5f9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3094,6 +3094,14 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
         show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
       omega
 
+theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by
+  apply eq_of_toInt_eq
+  simp [toInt_neg, toInt_add, Int.neg_add, Int.add_neg_eq_sub]
+
+theorem add_neg_eq_sub {x y : BitVec w} : x + - y = (x - y) := by
+  apply eq_of_toInt_eq
+  simp [toInt_neg, Int.sub_eq_add_neg]
+
 /- ### add/sub injectivity -/
 
 @[simp]
@@ -3262,6 +3270,12 @@ protected theorem neg_mul_neg (x y : BitVec w) : -x * -y = x * y := by simp
 
 protected theorem neg_mul_comm (x y : BitVec w) : -x * y = x * -y := by simp
 
+theorem neg_add_mul_eq_mul_not {x y : BitVec w} :
+    - (x + x * y) = x * ~~~ y := by
+  rw [neg_add, sub_toAdd, ← BitVec.mul_neg, neg_eq_not_add y, mul_add,
+    BitVec.mul_one, BitVec.add_comm, BitVec.add_assoc, BitVec.add_right_eq_self,
+    add_neg_eq_sub, BitVec.sub_self]
+
 /-! ### le and lt -/
 
 @[bitvec_to_nat] theorem le_def {x y : BitVec n} :