[This is problem 16.41 in Barwise & Etchemendy's "Language, Proof, and Logic".]
The only premise given is $\forall{x}\forall{y}\ (x<y \iff \exists z (x+s(z)=y))$
From this, it asks for a formal proof of: $\forall{x}\exists{y}\ x<y$
This is easy if we can appeal to the Peano Axioms; however, none of them listed as premises in this exercise.
The instructions for this section say: "Use [proof software] Fitch to construct formal proofs of the following theorems from the Peano Axioms plus the definition of <. In the corresponding Exercise file, you will find as premises only the specific axioms needed to prove the goal theorem."
Moreover, on 16.41 there is an explicit hint: "Notice that the Exercise file contains the definition of < but none of the Peano Axioms! So although this follows from Exercise 16.40 [$\forall x x<s(x)$], you won't be able to use your proof of that that[sic] as a lemma."
I'm stumped and confused. I apparently can't use any Peano Axioms, but if that's true, how am I supposed to use the given premise containing the successor function? Don't we need at least a few PA to define how that object behaves under addition?
Is this proof possible as described, or what am I missing? Hints only, no solutions, please!