Reading the explanations of Stephan Merz in the thread "pvs, temporal logic and stacks",
it comes to my mind it was the first time I was understanding how the Peano.tla file is made.
Obviously with the CHOOSE construction and an assumption that guarantees the existence
of Nat, Succ and Zero you can achieve what you want.
(It means at least that sometimes a piece of explanation in the spirit of literate programming can help.)
Some more remarks however.
Here is the definition of the natural numbers in Metamath (the definition is close to TLA+ definition except it is defined
as a subset of the real numbers here).
There is an intersection at the beginning to remove the garbage implied by induction definition.
I suppose
> \A S \in SUBSET N : (Z \in S) /\ (\A n \in S : Sc[n] \in S) => (S = N)
has the same role in Peano.tla?
Peano postulates are:
4 implies that suc is an injection. I'm not sure that this is the case in the TLA+ formalization.
Wikipedia also requires suc is an injection.
Final remark. What Peano.tla is good for? Because it seems that TLAPS
relies on SMT solvers every time aritmetics are involved.
FL