Context: I keep running into circular reasoning in attempting to derive strong induction (more generally "induction" whether it be weak or strong) from the well-ordering principle. Assume:
Peano Axioms w/ Well-Order: (I realize these are presented semi-informally)
(P1) $\ \exists x[x\!=\!1]$;
(P2) $\ $there exists an unary ("successor") function $S$ on $\mathbb{N}$ (i.e., $x\!\in\!\mathbb{N}\rightarrow S(x)\!\in\!\mathbb{N}$);
(P3) $\ \forall x[S(x)\!\neq\!1]$;
(P4) $\ \forall x\forall y[x\!\neq\!y\rightarrow S(x)\!\neq\!S(y)]$
(P5') $\ $Well-Ordering Principle: Every non-empty set includes a least-element: $$ \forall B\Big[\emptyset\!\subset\!B\!\subseteq\!\mathbb{N}\longrightarrow\exists m\big[m\!\in\!B\wedge\forall p[p\!\in\!B\rightarrow m\!\leq\!p]\big]\Big] $$ Note: Since I am trying to show the logical equivalency between Induction and the Well-Ordering Principle, I am assuming the latter as an axiom and treating the former as a theorem (below). The relation $\leq$ used above is defined next.
Order Relation
(O1) $\ x\!<\!y\leftrightarrow\exists z[x\!+\!z\!=\!y]$
(O2) $\ x\!\leq\!y\leftrightarrow[x\!=\!y\vee x\!<\!y]$
Addition (since order above is defined with "$+$")
(A1) $\forall x[S(x)=x+1]$
(A2) $\forall x\forall y[x+S(y)=S(x\!+\!y)]$
With this as background, below is the theorem and proof I see most often (or some variation thereof) in textbooks and online forums.
Theorem: The Well-Ordering Principle (P5') implies the Strong Induction Principle.
Proof: Suppose $X\!\subset\!\mathbb{N}$ with: (1) $1\!\in\!X$, and (2) $\forall x[x\!<\!k\rightarrow x\!\in\!X]\rightarrow k\!\in\!X$. Assume $X'\!\equiv\!\mathbb{N}\setminus X$ is non-empty. From Well-Ordering Principle (P5'), $X'$ includes a least element $m$. From (1), $m\!\neq\!1$. Since $m$ is the least element of $X'$, then all $x\!<\!m$ must belong to $X$. However, property (2) implies that $m\!\in\!X$, a contradiction. Thus, $X'$ must be empty and $X\!=\!\mathbb{N}$.
My problem is with the highlighted sentence above, which appears to me to require the result that $\neg(m\!\leq\!x)\leftrightarrow x\!<\!m$, which I believe is based on the Trichotomy Property (exactly one of $x\!<\!y$, $x\!=\!y$, $x\!>\!y$ holds). However, the only proof of the Trichotomy Property (that I am aware of) based on the above axioms/definitions alone uses Induction (see Thm 4.1c). Thus, it appears the reasoning is circular (induction is used to prove an intermediate result that is then used to prove induction).
Question: Assuming my understanding above is correct, my question simply put is this: does a proof exist of the Trichotomy Property for $<$ as defined above that does not require a proof based on induction?