feat: USize.size inequalities

[tydeu]

This PR adds the theorems le_usize_size and usize_size_le, which make proving inequalities about USize.size easier.

It also deprecates usize_size_gt_zero in favor of usize_size_pos (as that seems more consistent with our naming covention) and adds USize.toNat_ofNat_of_lt_32 for dealing with small USize literals.

It also moves USize.ofNat32 and USize.toUInt64 to Init.Data.UInt.Basic as neither are used in Init.Prelude anymore.

[tydeu]

These inequalities could also be named USize.le_size and USize.size_le, but I stuck with the current usize_size convention. This also avoids a clash with batteries, which already defines them and uses 2 ^ _ to represent the size instead of the computed value. I used the computed value as that is also current core convention.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6203 has successfully built against this PR. (2024-11-25 00:02:56) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 43dfc2a25fc64095fb76d576802a70d88773fea8 --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-25 13:49:54)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 43dfc2a25fc64095fb76d576802a70d88773fea8 --onto 20acc72a29a8bb4d55223651caa0553ffa82ac88. (2024-11-26 04:58:06)