TITLE: $n \in \mathbb{N} \wedge n>0 \iff \exists r \in \mathbb{N},n=r+1$
QUESTION [0 upvotes]: I found that this theorem is used many times, but I'm not sure if my below proof is correct or not. Of course, we can only use Peano's axioms and the definitions of addition and order $>$. I feel that any proof for this theorem will be short. I'm very happy to see other proofs for this theorem.
Theorem:

$n \in \mathbb{N} \wedge n>0 \iff \exists r \in \mathbb{N},n=r+1$

Proof:


$n \in \mathbb{N} \wedge n>0 \implies \exists r \in \mathbb{N},n=r+1$

It is true that $1>0$ and $1=0+1$. Thus the theorem is true for $n=1$.
Assume the theorem is true for $n=k$.
$k+1=(k)+1 \implies$ The theorem is true for $n=k+1$
By principle of induction, the theorem is true for all $n \in \mathbb{N}$.

$n \in \mathbb{N} \wedge n>0 \Leftarrow \exists r \in \mathbb{N},n=r+1$

$\exists r \in \mathbb{N},n=r+1 \implies \exists r \in \mathbb{N} (n=(r+1)+0) \wedge (n \neq 0) \implies n\geq 0 \wedge n \neq 0 \implies n >0$

REPLY [0 votes]: Correct; the proof is by induction and relies on Peano axioms.
We can simplify it a little bit expressing the theorem as follows:

$n \ne 0 \to \exists r \ (n=r+1)$.

Basis : $n=0$ is straightforward using the Ex falso tautology: $P \to (\lnot P \to Q)$.
Induction step : the induction hypothesis is not really necessary. 
Consider $n+1$; by axiom : $\forall x \ \lnot (0=x+1)$ we have that $n+1 \ne 0$ and by equality axioms we have : $n+1=n+1$ and thus, by existential introduction : $\exists r \ (n+1=r+1)$.
{"set_name": "stack_exchange", "score": 0, "question_id": 2724880}