Move Nat translation into a proof-producing preprocessing tactic

[Vtec234]

We currently translate Nat-based expressions in the smt tactic as Ints greater than zero. However this translation is not proof-producing, and it will cause issues for proof reconstruction when the solver has proved something about a positive integer, but the Lean goal is still about natural numbers. We agreed that the way to go here is to have a separate smt_nat_to_int (or something) preprocessing tactic which provably rewrites the goal to talk about positive integers. After running it, the goal would only include integers at which point the core smt translation can just raise an error whenever it encounters a Nat.

See here for a usage of the more general Transfer tactic in Isabelle/HOL.

[Vtec234]

There is a mathlib tactic zify which does a similar thing, although it seems to use casts rather than introducing explicit ≤ conditions.