Using Peano Axioms Prove That Greater Than Holds For Successor Functions

Question

In first order logic, $\ge$ can be defined as $\exists x(u = x + w)$.

I am trying to formally deduce a proof for:

$\exists x(u = x + w) \vdash \exists x(s(u) = x + s(w))$

I can use peano axioms and basic formal deduction rules. I'm just having a hard time figuring out how to start the question and always get confused if I should use induction or not. Kinda new to this and just looking for a hint on how to start or general guidance on how to approach the question.

If I'm replacing the bound variables with free variables to start, which I believe I should, I know my final step would most likely be to add the $\exists x$ back to the LSH of the proof.

Any help appreciated.

Edit: Forgot to just say domain is natural numbers

Answer 1

1. $∃x(u=x+w)$ ---premise

2. $u=a+w$ --- assumed [a] form 1) for $\exists$-elimination

3. $s(u)=s(a+w)$ --- from 2) by substitution axiom for equality

4. $s(u)=a+s(w)$ --- from 3) by axiom for $+$

5. $\exists x (s(u)=x+s(w))$ --- from 4) by $\exists$-introduction.

$\exists x (s(u)=x+s(w))$ --- from 2)-5) and 1) by $\exists$-elimination, discharging assumption [a].