feat: getLsb_sshiftRight

[bollu]

In the course of the development, I grabbed facts about right shifting over integers from mathlib4.

The core proof strategy is to perform a case analysis of the msb:

• If msb = false, then sshiftRight = ushiftRight.
• If msb = true. then x >>>s i = ~~~(~~~(x >>>u i)). The double negation introduces the high 1 bits that one expects of the arithmetic shift.

[bollu]

awaiting-review

[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 82666e5e7cfc541659459bd450f5f1b24a4080eb --onto 3035d2f8f689b52963f49b2414414913ca296953. (2024-05-15 17:54:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 73a0c73c7cc465ce8674eacaaa831e9ee0e95950 --onto d984030c6a683a80313917b6fd3e77abdf497809. (2024-05-23 14:25:36)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 73a0c73c7cc465ce8674eacaaa831e9ee0e95950 --onto b0c1112471a3f38859d9738184d21132b7d9cd0c. (2024-05-25 01:50:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 73a0c73c7cc465ce8674eacaaa831e9ee0e95950 --onto fe17b82096bf4825d83a36f220d79a6dadebf5c8. (2024-05-27 11:09:32)

[bollu]

awaiting-review

[bollu]

awaiting-review

[semorrison]

Many stylistic comments, but I'm now satisfied that the main proof really requires this much talking about Int.negSucc! Hopefully we can merge soon.

[tobiasgrosser]

awaiting-author

[bollu]

@semorrison I've cleaned up the proof, thanks a lot for your detailed stylistic comments.

[bollu]

awaiting-review