feat: normalize divisibility constraints and tighten bounds modulo divisors in `lia`

This PR makes `lia` solve goals with large-modulus divisibility constraints, such as `65536 ∣ 10 * x ⊢ 32768 ∣ x`, without a Cooper case split per residue.

Constraints `d ∣ p` are normalized by reducing the coefficients modulo `d` (balanced) after multiplying by the inverse of the leading coefficient when coprime to `d`, so `32768 ∣ 5*x` becomes `32768 ∣ x`. Bound tightening now applies whenever the value of a bound is known modulo a divisor of `d`, generalizing the previous exact-coefficient match.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>