refactor: redefine unsigned fixed width integers in terms of BitVec

[hargoniX]

I made a few choices so far that can probably be discussed:

• got rid of modn on UInt, nobody seems to use it apart from the definition of shift which can use normal mod
• removed the previous defeq optimized definition of USize.size in favor for a normal one. The motivation was to allow OfNat to work which doesn't seem to be necessary anymore afaict.
• Minimized uses of .val, should we maybe mark it deprecated?
• Mostly got rid of .val in basically all theorems as the proper next level of API would now be .toBitVec. We could probably re-prove them but it would be more annoying given the change of definition.
• Did not yet redefine log2 in terms of BitVec as this would require a log2 in BitVec as well, do we want this?
• I added a couple of theorems around the relation of < on UInt and Nat. These were previously not needed because defeq was used all over the place to save us. I did not yet generalize these to all types as I wasn't sure if they are the appropriate lemma that we want to have.

[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 273b7540b2ad6288344869a7e2324de376aada5a --onto adfd6c090ef7d6bdcc8f69c5dd6f919b1b71cab3. (2024-09-12 14:38:38)
• 💥 Mathlib branch lean-pr-testing-5323 build failed against this PR. (2024-09-23 10:04:20) View Log
• 💥 Mathlib branch lean-pr-testing-5323 build failed against this PR. (2024-09-23 10:36:03) View Log
• 💥 Mathlib branch lean-pr-testing-5323 build failed against this PR. (2024-09-23 11:57:56) View Log
• 🟡 Mathlib branch lean-pr-testing-5323 build against this PR was cancelled. (2024-09-23 13:23:04) View Log
• 💥 Mathlib branch lean-pr-testing-5323 build failed against this PR. (2024-09-23 14:07:28) View Log
• 💥 Mathlib branch lean-pr-testing-5323 build failed against this PR. (2024-09-23 14:33:59) View Log
• 💥 Mathlib branch lean-pr-testing-5323 build failed against this PR. (2024-09-24 00:27:33) View Log
• ❗ 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 10:32:27)

[kim-em]

Looks great.

Could you leave a deprecation in place for modn, just in case there is a downstream user?

Agree to marking .val as deprecated, but it can also happen later.

BitVec.log2 sounds good, but probably deserves a different name, and can happen later.

Would you mind rebasing onto nightly-with-mathlib so we can check to see how much we have disturbed downstream. (Ideally nothing, but I'm be pleasantly surprised if that were the case.)

[kim-em]

(I'm keen to have this in, as I'm thinking about Fin refactors.)

[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 79930af11e5b6e78e77534d7670169ea5f5924c5 --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-09 08:29:23)