feat: add BitVec.toInt_[intMin|neg|neg_of_ne_intMin ]

[tobiasgrosser]

No description provided.

[tobiasgrosser]

I am not yet very happy with two_pow_pred_sub_two_pow and related functons:

• I currently have two versions of two_pow_pred_sub_two_pow and would really like to have one canonical version. The one without explicit casts looks a bit nicer, but then has these heterogenous @HPow.hPow Int Nat Int instHPow 2 (w - 1) : Int which do not match with any of the 2 ^ w lemmas in Nat.

• Is there a reason Int.natCast_pow is not tagged as norm_cast?

• I had to introduce theorem natCast_two_pow (n : Nat) : ((2^n : Nat) : Int) = (2: Int) ^ n := by to make 2 ^ w lemmas apply.
  Obvious, it would be nice to generalize this for any positive constant.

  I tried to tag this lemmas as norm_cast, but this just led to more heterogenous pows, rather than to turn heterogenous pows into nat-pows with int-casts at the root.

[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 6b0d4e50c0bb462ad86a2d19caad477ced1ebe37 --onto e551a366a0bbb27d5f853cc8e87cbd381a76ffc0. (2024-09-24 07:43:18)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d2c7fc1d92a1049f04bba1b16c0a1cfae845e00 --onto e551a366a0bbb27d5f853cc8e87cbd381a76ffc0. (2024-09-24 11:57:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d2c7fc1d92a1049f04bba1b16c0a1cfae845e00 --onto 94de4ae96413d83bf0964d83500be0d3cdeff18f. (2024-09-24 19:11:29)