feat: dynamic variable reordering before large Cooper splits in `lia`

This PR makes `lia` reorder its variables instead of enumerating a Cooper case split with many cases, which fixes goals such as a three-limb counter increment that previously needed a `2^32`-way split.

A split on `x` has as many cases as the coefficient of `x` in the conflicting bounds. The search now abandons such a split, orders `x` first so that it becomes a parameter of those bounds, and restarts; the conflict then surfaces at a variable with a smaller coefficient. Two new options control it: `liaReorderCases` (default 16), the case count above which a reordering is requested, and `liaReorders` (default 8), the maximum number of reorderings per goal, with `0` disabling the mechanism.

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