defining inequality of natural numbers by case-analysis If I add to Peano Arithmetic a relation (predicate?) symbol $\leq$ and an axiom $\forall n\forall m(n\leq m \leftrightarrow n=m \lor S(n)\leq m)$, can I prove $\forall n\forall m(n\leq m \to n\leq S(m))$?
Related question: How to compare Peano numbers?
 A: You can see this post for reference to the logical theory of definition.
In oder to add to a first-order language a new predicate symbol $P$, we have to introduce an axiom defining it.
The defining axiom must be : $P(x_1, \ldots, x_n) \leftrightarrow \varphi(x_1, \ldots, x_n)$, where $\varphi$ is a formula of the "original" language, and thus must not contain the predicate $P$.
In first-order arithmetic with Peano's axiom we can introduce the binary predicate (or relation) $<$ through the axiom :

$n < m \leftrightarrow \exists z (m=n+S(z))$

and then :

$n \le m \leftrightarrow n < m \lor n = m$.

With these abbreviations, we can prove :


$n \le m \leftrightarrow n < S(m)$.


See Stephen Cole Kleene, Introduction to Metamathematics (1952) : $ ✳138a$, page 188.


Proof
For lemmas, I'll use the original Kleene's numeration; for Peano's axioms I'll call them $P1-P7$, following the order in Wiki's page.  
Some preliminary lemmas:
$✳135b : 0 < S(n)$; proof from axioms $P3-P4$ : recursive axioms for sum.
$ ✳136 : 0 \le n$; proof by Induction on $n$, using $✳135b$.
$ ✳137 : n = 0 \lor (\exists m)(n = S(m))$; proof by cases from $✳136 : 0 < n \lor 0 = n$.

The following is an expanded version of the three-lines proof in Kleene's book of :

$ ✳138a : n \le m \leftrightarrow n < S(m)$.

Proof : 
step 1
$n < S(m) \leftrightarrow (\exists z)(S(m)=n + S(z))$ --- abbreviation

[1] assume for $\exists$E : $S(m)=n+S(z)$;

$z = 0 \lor (\exists w)(z=S(w))$ --- from $✳137$


[1a] assume $z=0$


from [1] : $S(m)=n+S(0)$ 
$S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$ --- by $\lor$I
Thus : $c=0, S(m)=n+S(z) \vdash S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$ --- by $\exists$E.


[1b] assume $(\exists w)(z=S(w))$


In the same way, by $\exists$E, we prove : $(\exists w)(z=S(w)), S(m)=n+S(z) \vdash S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$.
From [1a] and [1b] follows (proof by cases and $\rightarrow$I) : 

$n < S(m) \rightarrow S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$.

=\=\=\=

[2] assume $S(m)=n+S(0)$; by $\exists$I : $(\exists z)(S(m)=n+S(z))$;

also :  $(\exists w)(S(m)=n + S(S(w))) \vdash (\exists z)(S(m)=n+S(z))$.
Then $S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w))) \rightarrow (\exists z)(S(m)=n+S(z))$ --- proof by cases and $\rightarrow$I.
Thus: 

$S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w))) \rightarrow (n < S(m))$ --- abbreviation.

=\=\=\=
From [1] and [2] and $\leftrightarrow$I : 


$n < S(m) \leftrightarrow S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w)))$


=\=\=\=
=\=\=\=
step 2

[1] Assume : $S(m)=n+S(0)$;

it follows that : $S(m)=S(n+0)$, by axiom $P4$, and : $m=n+0$, by axiom $P2$, and $m=n$.
Thus : $S(m)=n+S(0) \rightarrow m=n$.
In the same way : $m=n \rightarrow S(m)=n+S(0)$. 

Thus, by $\leftrightarrow$I : $m=m \leftrightarrow S(m)=n+S(0)$.

=\=\=\=

[2] Assume $(\exists w)(S(m)=n+S(S(w)))$;

assume for $\exists$E : $S(m)=n+S(S(w))$; then $S(m)=S(n+S(w))$, and so : $m=n+S(w)$ and finally : $(\exists w)(m=n+S(w))$, by $\exists$I.
Thus :
$(\exists w)(S(m)=n+S(S(w))) \rightarrow  (\exists w)(m=n+S(w))$.
In the same way : $(\exists w)(m=n+S(w)) \rightarrow (\exists w)(S(m)=n+S(S(w)))$
Finally : 

$(\exists w)(m=n+S(w)) \leftrightarrow (\exists w)(S(m)=n+S(S(w)))$ --- by $\leftrightarrow$I.

=\=\=\=
=\=\=\=
step 3
From step 1 we have : $n < S(m) \leftrightarrow S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w)))$.
From step 2 we have : $(\exists w)(m=n+S(w)) \leftrightarrow (\exists w)(S(m)=n+S(S(w)))$.
We need also the fact that : $S(m)=n+S(0)=S(n+0)=S(n) \leftrightarrow m=n$.
Using tautologies [see $✳29a/b$, page 116] : $A \leftrightarrow B \vdash (A \lor C) \leftrightarrow (B \lor C)$ and $A \leftrightarrow B \vdash (C \lor A) \leftrightarrow (C \lor B)$, we have : 

$n < S(m) \leftrightarrow m=n \lor (\exists w)(m=n+S(w))$

and finally, with the abbreviation for $n < m$ :


$n < S(m) \leftrightarrow m=n \lor n < m$


which is :



$n < S(m) \leftrightarrow n \le m$.





Notes
(A) Equivalently, we can start with :

$n \le m \leftrightarrow \exists z (m=n+z)$

and then define :

$n < m \leftrightarrow n \le m \land n \ne m$.


(B) We can instead use $<$ as a primitive symbols, adding to the usual (firts-oder) Peano's axioms the following recursive definition of $<$ :

$\forall x \lnot (x < 0)$
$\forall x \forall y (x < S(y) \leftrightarrow (x < y \lor x = y))$.

