perf: use `Int.rec`-based arithmetic in `lia` certificates

This PR adds the module `Init.Data.Int.Kernel` with `Int.add_k`, `Int.mul_k`, and `Int.neg_k`, versions of `Int` arithmetic written with `Int.rec`, `Bool.rec`, and `Nat` operations that the kernel evaluates on literals, together with proofs that they agree with the standard operations. The kernel-reduction helpers used by `lia` certificates now use them, and `eq_le_subst_nonneg_cert`, `eq_le_subst_nonpos_cert`, and `diseq_eq_subst_cert` use `Poly.coeff_k`, so the kernel checks these certificates without unfolding `match`-based definitions.

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