feat: bound grind case splits by the size of the search tree

This PR replaces the `grind` option `splits` with `branches`, which limits the total number of branches that case splitting may create during a proof search (default 1024). Previously, `grind`, `lia`, and the related tactics allowed at most 9 case splits along each branch of the search, so a goal with a long chain of cheap case splits failed even when its proof was tiny. For example, a hypothesis `x ≤ 0 ∨ 100 ≤ x ∨ x = 2 ∨ x = 4 ∨ … ∨ x = 36` whose disjuncts are each refuted immediately needed 17 case splits in a row and exceeded the limit. Such goals are now proved with the default configuration, while the total amount of case splitting stays bounded.

A case split with `n` cases creates `n - 1` new branches, and case splits that turn out to be irrelevant to the proof are not counted. In `grind => …` mode, each `finish` starts with a fresh budget. When the limit is reached, the error message says so, e.g., "`lia` has failed after reaching the threshold `(branches := 1024)`", and `grind (branches := n)` raises it.

Migration:
* `splits` is deprecated and reports a warning, which can be disabled with `set_option linter.deprecated false`.
* `splits := 0` still disables case splitting, and is equivalent to `branches := 0`.
* Other values of `splits` are ignored. If a proof needs more case splitting than the default allows, use `branches := n`.
* `grobner (splits := n)` no longer enables case splitting. Use `grobner (branches := n)`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>