diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 41a662e47..5600621f8 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -810,6 +810,24 @@ lemma toInt_zero_iff (w : Nat) (x : BitVec w) : BitVec.toInt x = 0 ↔ x = 0 :=
 lemma toInt_nonzero_iff (w : Nat) (x : BitVec w) : BitVec.toInt x ≠ 0 ↔ x ≠ 0 := by
   simp [toInt_ne]
 
+@[simp]
+lemma carry_and_xor_false : carry i (a &&& b) (a ^^^ b) false = false := by
+  induction i
+  case zero =>
+    simp [carry, Nat.mod_one]
+  case succ v v_h =>
+    simp only [carry_succ, v_h, Bool.atLeastTwo_false_right, getLsb_and,
+      getLsb_xor, Bool.and_eq_false_imp, Bool.and_eq_true, bne_eq_false_iff_eq,
+      and_imp]
+    intros; simp [*]
+
+@[simp]
+theorem and_add_xor_eq_or {a b : BitVec w} : (a &&& b) + (a ^^^ b) = a ||| b := by
+  ext i
+  rw [getLsb_add (by omega), getLsb_and, getLsb_xor, getLsb_or]
+  simp only [Bool.bne_assoc]
+  cases a.getLsb ↑i <;> simp [carry_and_xor_false]
+
 end BitVec
 
 -- Given (a, b) that are less than a modulus m, to show (a + b) % m < k, it suffices to consider two cases.