After defining things like natural numbers and addition, I'd like to prove some things about the operator $\leq$ and ask if they are correct.
Definition 1: Let $a$ and $b$ be natural numbers. We say that $a \geq b$ (or $b \leq a$) iff we have $a = b + m$ for some natural number $m$.
Definition 2: We say natural number $a$ is positive iff $a \neq 0$.
Order is reflexive: $a \geq a$. Proof: $a = a + m$ reduces to $0 = m$ by cancellation law, so this relationship holds for $m=0$.
Order is transitive: If $a \geq b$ and $b \geq c$, then $a \geq c$. Proof: Let $j,k$ be natural numbers. Then we can write $a = b + j$ and $b = c + k$. This also means $a = c + k + j$. Let $m = k + j$, a natural number. Then we can write $a = c + m$, and therefore $a \geq c$.
Order is anti-symmetric: If $a \geq b$ and $b \geq a$ then $a=b$. Proof: Let $j,k$ be natural numbers. Then by definition we can write $a = b + j$ and $b = a + k$. By substitution, $a = a + k + j$. By cancellation law, $0 = k + j$. By the two subclaims 3.a. and 3.b. we have $k=j=0$. So $a = b + 0$ and $b = a + 0$, which in both cases simplify to $a = b$.
3.a. Subclaim: If $a$ is positive natural number, then $a+b$ is a positive natural number for natural number $b$. Proof: We use induction. If $b=0$, then $a+0 = a$ which is a positive natural number. For the inductive step, suppose $a+b$ is a positive natural number. Then we must show $a+S(b)$ is a positive natural number. $a+S(b) = S(a+b)$ by the definition of addition, which cannot be $0$ by Peano's third axiom.
3.b. Subclaim If $0 = a+b$ for natural numbers $a,b$, then $a=0$ and $b=0$. Proof: Suppose for the sake of contradiction that $a \neq 0$ or $b \neq 0$. If $a \neq 0$, then $a$ is positive. But if $a$ is positive, $a+b$ is positive, and cannot be $0$ by subclaim 3.a. Likewise, if $b \neq 0$, $b + a$ is positive, and cannot be $0$ either.
For 1, I think a little cleaner is to go the other way around: we know that $a=a+0$, and therefore $a=a+m$ for some $m$, and therefore $a \le a$.
It's a little cleaner, for if you start with $a=a+m$, and then say "by cancellation law this reduces to $m=0$", you seem to be merely saying that $a=a+m$ implies that $m=0$, but you need to show just the other way around: that $m=0$ implies $a=a+m$, and hence that there is some $m$ such that $a=a_m$
Also: going this way, you don;t need to refer to any kind of cancellation law which, if you start out with basic axioms, is a good bit more complicated than proving any of these!