diff --git a/SSA/Projects/InstCombine/Alive.lean b/SSA/Projects/InstCombine/Alive.lean
index d6a214af9..73d877f91 100644
--- a/SSA/Projects/InstCombine/Alive.lean
+++ b/SSA/Projects/InstCombine/Alive.lean
@@ -30,3 +30,5 @@ import SSA.Projects.InstCombine.LLVM.Lemmas
 import SSA.Projects.InstCombine.Test
 -- Examples for the paper
 import SSA.Projects.InstCombine.PaperExamples
+-- Proofs from Hackers Delight Book
+import SSA.Projects.InstCombine.HackersDelight
diff --git a/SSA/Projects/InstCombine/HackersDelight.lean b/SSA/Projects/InstCombine/HackersDelight.lean
new file mode 100644
index 000000000..576f0097e
--- /dev/null
+++ b/SSA/Projects/InstCombine/HackersDelight.lean
@@ -0,0 +1,14 @@
+import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Bitblast
+
+namespace HackersDelight
+
+namespace Ch1
+
+theorem neg_eq_not_add_one {x : BitVec w} : - x = ~~~ x + 1 := by
+  apply BitVec.neg_eq_not_add
+
+end Ch1
+
+end HackersDelight