decide +kernel: || short-circuits; Nat.choose k 2 not slow alone

Measured on Lean/Mathlib v4.35.0. The kernel evaluates Bool || lazily: (true || slow 2000000) = true by decide +kernel passes, while (slow 300000 || true) = true fails with '(kernel) deep recursion detected' (slow folds a Bool check over List.range n). So put cheap disjuncts first in kernel-evaluated checkers. By contrast, the advice to replace Nat.choose k 2 with k*(k-1)/2 did not show up in isolation: summing choose k 2 over List.range 6000 took 8 s wall, against 11 s for the formula, with about 5 s of that being the import Mathlib baseline. Measure inside your own checker before rewriting.