feat: add BitVec.sdivOverflow definition and lemmas for overflow in signed and unsigned division

[luisacicolini]

This PR introduces the lemmas to check overflow conditions on signed and unsigned division BitVec.sdivOverflow and BitVec.not_udivOverflow (given that unsigned division never overflows), according to the definitions here.
The core proofs majorly relies on omega, when the bounds of the division are precise enough. This required introducing numerous Int.sdiv_* lemmas.

Co-authored by @bollu.

[leanprover-community-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 b0e58d3387ec103287ac56aea95e4cecd9968982 --onto 635af865bf52013210057ebfb99bec4c04f40cab. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-24 23:38:59)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b0e58d3387ec103287ac56aea95e4cecd9968982 --onto 2edfe2e9cffd55e3c79291628ae091b942291ec9. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-01 15:46:30)

[luisacicolini]

changelog-library

[bollu]

I believe in Int, the theorems are called as div_... rather than sdiv_...? So I'd at the very least change that. We also have theorems that use ge, which is not the simp normal form:

• sdiv_neg_ge_two_ge
• sdiv_neg_le_neg_two_ge

[bollu]

Suggested change

	theorem sdiv_neg_ge_two_ge (x y : Int) (hy' : 2 ≤ y) (hx' : x < 0) :
	theorem div_le_of_two_le_of_lt_zero (x y : Int) (hy' : 2 ≤ y) (hx' : x < 0) :

I wonder what the canonical way of spelling x < 0 is in the theorem name: do we say lt_zero?

[bollu]

Suggested change

	theorem sdiv_pos_le_neg_two_le (x y : Int) (hy' : y ≤ -2) (hx' : 0 < x) :
	theorem sdiv_nonpos_of_le_neg_two_of_zero_lt (x y : Int) (hy' : y ≤ -2) (hx' : 0 < x) :

It would be good to have an English sentence that explains what's going on. Also, doesn't the theorem hold for a looser bound, when y <= -1? We should try to now generalize our statements, as the proof goes through.