# Prove strict well-order from Peano successor function

Is there a way to prove from (a variation) of the Peano successor function without induction that < is a strict well-order? Specifically, let $$m\leftarrowtail n$$ represent that $$n$$ is the successor of $$m$$ and assume the axioms

1. $$1\in N$$
2. if $$m\in N$$ then $$\exists! n\in N.m\leftarrowtail n$$
3. $$\neg \exists m.m\leftarrowtail 1$$
4. if $$n\in N$$ and $$n\ne 1$$ then $$\exists! m\in N.m\leftarrowtail n$$

Note that I have combined two Peano axioms into one for axiom 2 (existence and uniqueness of successors), and added a new axiom for axiom 4 (you can't prove unique predecessors without induction, and you need them to prove induction from well-orderedness).

The transitive closure of the $$\leftarrowtail$$ relation is the normal $$<$$ relation from arithmetic. My question is, can you prove that this transitive closure is a well-order without induction? I think I can prove it, but I'm having trouble formalizing the idea.

Consider for example the linear order $$(\mathbb{N}\times\{0\})\cup(\mathbb{Z}\times \{1\})$$ ordered by setting $$(a,i)<(c,j)$$ iff $$i or $$i=j$$ and $$a. Intuitively, this looks like a copy of $$\mathbb{N}$$ followed by a copy of $$\mathbb{Z}$$. This linear order has a first element $$(1,0)$$ and a successor operation which together satisfy all your axioms, but it is clearly not well-ordered.