chore: move BitVec.udiv/umod/sdiv/smod after add/sub/mul/lt

[tobiasgrosser]

Divison proofs are more likely to depend on add/sub/mul proofs than the other way around. This cleans up #5609, which added division proofs that rely on negation to already be defined.

[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 0178f2b70df112a916efaaf8acede9ccea12b950 --onto a4fda010f3d44c02393d5afd5cf05509989daf63. (2024-10-06 07:39:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9dac514c2fc80d3f60076314ad30a993a7b2c22f --onto a4fda010f3d44c02393d5afd5cf05509989daf63. (2024-10-07 13:20:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d6553029cb589669f75b8eb68f0e7d1bd8147ff --onto 1d8555fe0bdd02c82664446309b2e167ac89c9e9. (2024-10-13 18:01:14)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47e0430b07cdd2569046e531fb44eba5f6ffc3d0 --onto 1d8555fe0bdd02c82664446309b2e167ac89c9e9. (2024-10-13 20:06:45)

[bollu]

LGTM, and I ran a diff, and the only change was to make a terminal simp into a simp only:

bollu@paracompact-2 ~/temp [1]> diff a b
87c87
<   <;> simp [h'', h''']
---
>   <;> simp only [h'', h''', ↓reduceIte, toNat_ofNat, Nat.zero_mod, toNat_umod]

[tobiasgrosser]

LGTM, and I ran a diff, and the only change was to make a terminal simp into a simp only:

bollu@paracompact-2 ~/temp [1]> diff a b
87c87
<   <;> simp [h'', h''']
---
>   <;> simp only [h'', h''', ↓reduceIte, toNat_ofNat, Nat.zero_mod, toNat_umod]

This is intentional.

[bollu]

Since it was intentional, LGTM