From c9e8dbbd443ea6f8fab256f30a9a9717bc6874dd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 5 Nov 2024 15:33:44 +1100
Subject: [PATCH] .

---
 src/Lean/SimpLC/Whitelists/BitVec.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/Lean/SimpLC/Whitelists/BitVec.lean b/src/Lean/SimpLC/Whitelists/BitVec.lean
index db4547beb905..6f6bfd5c3f03 100644
--- a/src/Lean/SimpLC/Whitelists/BitVec.lean
+++ b/src/Lean/SimpLC/Whitelists/BitVec.lean
@@ -56,11 +56,8 @@ simp_lc whitelist BitVec.udiv_one BitVec.udiv_self
 -- example (x : BitVec 1) : x = if x = 0#1 then 0#1 else 1#1 := by bv_decide
 simp_lc whitelist BitVec.udiv_eq_and BitVec.udiv_self
 
--- TODO: move to library
-@[simp] theorem BitVec.ofFin_zero_sub {w : Nat} (i : Fin (2^w)) :
-    ofFin (0 - i) = - ofFin i := by
-  apply BitVec.eq_of_toNat_eq
-  simp [Fin.coe_sub]
+example (w : Nat) : w = 0 → 0#w = 1#w := by rintro rfl; simp
+simp_lc whitelist BitVec.sdiv_self BitVec.sdiv_one
 
 /-
 The actual checks happen in `tests/lean/run/simplc.lean`.