From 16aa80306ece730b0526cd27a0a72acd1da68246 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 30 Aug 2024 12:37:11 +1000
Subject: [PATCH] feat: Nat.bitwise lemmas (#5209)

---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index cca861cde6..d2eecf0eee 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -463,6 +463,10 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
   rw [testBit_and]
   simp
 
+theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 := by
+  apply Nat.eq_of_testBit_eq
+  simp [testBit_and, ← testBit_add_one]
+
 /-! ### lor -/
 
 @[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
@@ -486,6 +490,10 @@ theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y
   rw [testBit_or]
   simp
 
+theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
+  apply Nat.eq_of_testBit_eq
+  simp [testBit_or, ← testBit_add_one]
+
 /-! ### xor -/
 
 @[simp] theorem testBit_xor (x y i : Nat) :
@@ -508,6 +516,10 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a
   rw [testBit_xor]
   simp
 
+theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 := by
+  apply Nat.eq_of_testBit_eq
+  simp [testBit_xor, ← testBit_add_one]
+
 /-! ### Arithmetic -/
 
 theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat) :