Formal Proof of "No Largest Number"

Question

I need to create a formal proof of there not being the largest number, with only the definition of "less than" being given with Peano arithmetic. $s(x)$ means successor of $x$ or $x + 1$.

$$ \text{Premise}\\ \forall x\forall y (x \lt y \iff \exists z(x + s(z) = y)\\ \text{Prove}\\ \forall x \exists y (x < y) $$

I've tried proof by contradiction, but the resources online don't seem to translate well into a formal proof. In particular, the strategy of "assume there is a largest number, add one, done" doesn't really translate with formal proof steps.

Answer 1

Solved!

The key to solving this was with "creating the right half" of the original premise: $\exists z (x + s(z) = y)$

Answer 2

So you want to prove that for all $x$, there exists a $y$ such that $x$ is less than $y$. To do that, imagine you are given an $x$ (maybe $x=99$) and try to come up with a $y$ that is greater than $x$. How about $x + 1$ (i.e., $100$ if $x = 99$)? So there's your proof: as $y = x + 1 > x$ for any $x$, then for all $x$, there exists a $y$ such that $x < y$.

Proof by contradiction is best regarded as a last resort: to be used only if working forward from the positive information that you have isn't getting you anywhere.

Answer 3

Using the idea of Barry Cipra in the comments:

$$\forall x \exists y~(y=s(x)) \\ \forall x \exists y \exists w ~(x+y=x+s(x)=w) \\ (\forall x \exists z (=x)~(x +s(z)=w)) \Rightarrow x \lt w \Rightarrow \exists w~(x \lt w)$$