Find the representation in Peano system It's known that all recursive functions are representable in Peano arithmetic. I am trying to find representation of subtraction function 
$f(x,y)= \left\{\begin{matrix}
x-y &if& x>y\\ 
0 & if& x \leq y
\end{matrix}\right.$
I think its representation formula is $R(x,y,z) \leftrightharpoons (x>y\Rightarrow  x+z=y) \wedge (x\leqslant y \Rightarrow z=0)$.
I have to show that 
1) If $f(a,b)=c$ then $\vdash R(a,b,c)$
2) $\vdash\exists _{1}z R(x,y,z) $
How to show it?
 A: Proof sketch
(1) is straightforward. Argue by cases.
If $f(a, b) = 0$, then not-($a > b$). So $PA \vdash \neg(\overline{a} > \overline{b})$ (why?) and hence $PA \vdash \overline{a} > \overline{b} \to \overline{a} + \overline{c} = \overline{b}$. Also $PA \vdash \overline{0} = \overline{0}$ and hence $PA \vdash \overline{a} \leq \overline{b} \to \overline{0} = \overline{0}$. Putting things together, $PA \vdash R(\overline{a}, \overline{b}, \overline{c})$.
Similarly if $f(a, b) = c$, $c > 0$, then $a + c = b$ and so $PA \vdash \overline{a} + \overline{c} = \overline{b}$ hence $PA \vdash \overline{a} > \overline{b} \to \overline{a} + \overline{c} = \overline{b}$. Also not-$a \leq b$, so $PA \vdash \neg(\overline{a} \leq \overline{b})$ hence $PA \vdash \overline{a} \leq \overline{b} \to \overline{c} = \overline{0}$. Putting things together again, here too $PA \vdash R(\overline{a}, \overline{b}, \overline{c})$.
(2) Query: Are you sure you want to show $PA \vdash\exists _{1}z R(x,y,z)$ rather than the more usual $PA \vdash\exists _{1}z R(\overline{a},\overline{b},z)$? 
Anyway, to show (2), prove existence and uniqueness separately. I'll leave existence as an exercise.
For uniqueness, assume $R(x, y, z)$ and $R(x, y, z')$. Argue in $PA$ by cases from $x > y \lor x \leq y$. The first disjunct gives $x + z = y$ and $x + z' = y$ and you need to show (or assume) that those entail $z = z'$. The second disjunct gives $z = 0$ and $z' = 0$ and so $z = z'$. So either way $z = z'$, which completes the proof.
