feat: bitVec shiftLeft recurrences for bitblasting

[bollu]

@[simp]
theorem shiftLeftRec_zero (x : BitVec w₁) (y : BitVec w₂) :
    shiftLeftRec x y 0 = x <<< (y &&& twoPow w₂ 0)  := by
  simp [shiftLeftRec]

@[simp]
theorem shiftLeftRec_succ (x : BitVec w₁) (y : BitVec w₂) :
    shiftLeftRec x y (n + 1) =
      (shiftLeftRec x y n) <<< (y &&& twoPow w₂ (n + 1)) := by
  simp [shiftLeftRec]

theorem shiftLeftRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) (hn : n + 1 ≤ w₂) :
  shiftLeftRec x y n = x <<< (y.truncate (n + 1)).zeroExtend w₂ := by

These theorems are used for bitblasting shiftLeft in LeanSAT.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 18c97926a13bfc82c9266bf00483ab13c6acb64f --onto 62b6e5878981d1bb6d414f21b0c6f8d8a36e6834. (2024-06-27 10:48:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8959b2ca87a67cb88ab0828db3672384ad7302fe --onto 4d0b7cf66c140dd83f8c8634293047335a385026. (2024-07-03 07:32:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8959b2ca87a67cb88ab0828db3672384ad7302fe --onto 582d6e7f7168e0dc0819099edaace27d913b893e. (2024-07-10 13:21:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8959b2ca87a67cb88ab0828db3672384ad7302fe --onto 8ceb24a5e6782aac39fdb3bb2b47021ac38d0847. (2024-07-22 10:12:33)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8959b2ca87a67cb88ab0828db3672384ad7302fe --onto 5938dbbd14145c9b78f7645c4777f62a3fc8212c. (2024-07-23 15:53:44)

[bollu]

awaiting-review

[kim-em]

toNat_add_of_and_eq_zero will suffice: if there's only one sensible RHS, it doesn't need to be described in the name.

[kim-em]

Besides the renamings, and Alex's comment suggestion this now looks good to go!