feat: generalize theorem Nat.div_lt_div_right

[plp127]

This PR changes the statement of the theorem Nat.div_lt_div_right, whose conclusion is b / a < c / a ↔ b < c, to not require a ∣ b as an assumption.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c4e6b62c3d955ef20da94310797072f7c4c5fa2b --onto f2bcf2e8660ab2d16cf3cb50c8e127de0439a337. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-06 02:33:17)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c4e6b62c3d955ef20da94310797072f7c4c5fa2b --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-06 02:33:18)

[TwoFX]

Thanks!