From 9ef996259b20bfdce5fd2f83f2443b19b413daaa Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 27 Aug 2024 11:01:44 +1000
Subject: [PATCH] feat: add BitVec.intMax_add_one

---
 src/Init/Data/BitVec/Lemmas.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 4453a925ed..5bbaa37d78 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1836,4 +1836,10 @@ theorem getLsb_intMax (w : Nat) : (intMax w).getLsb i = decide (i + 1 < w) := by
   rw [← testBit_toNat, toNat_intMax, Nat.testBit_two_pow_sub_one, decide_eq_decide]
   omega
 
+@[simp] theorem intMax_add_one {w : Nat} : intMax w + 1#w = intMin w := by
+  simp only [toNat_eq, toNat_intMax, toNat_add, toNat_intMin, toNat_ofNat, Nat.add_mod_mod]
+  by_cases h : w = 0
+  · simp [h]
+  · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)]
+
 end BitVec