feat: Bitvector 0 equals bitvector 1 iff width is zero (#8202)

This PR adds an inference that was repeatedly needed when proving
`BitVec.msb_sdiv`, and is the symmetric version of
`BitVec.one_eq_zero_iff`

src/Init/Data/BitVec/Bitblast.lean

@@ -1501,7 +1501,6 @@ theorem sdiv_intMin {x : BitVec w} :
   by_cases h : x = intMin w
   · subst h
     simp
-    omega
   · simp only [sdiv_eq, msb_intMin, show 0 < w by omega, h]
     have := Nat.two_pow_pos (w-1)
     by_cases hx : x.msb

src/Init/Data/BitVec/Lemmas.lean

@@ -518,6 +518,10 @@ theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
   · rintro rfl
     simp
 
+/-- `0#w = 1#w` iff the width is zero. -/
+@[simp] theorem zero_eq_one_iff (w : Nat) : (0#w = 1#w) ↔ (w = 0) := by
+  rw [← one_eq_zero_iff, eq_comm]
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]