How do I prove that $\forall a \forall b(\neg a<b\iff b\leq a)$ [duplicate]

Question

The universe is the set of natural numbers including 0, which are defined in accordance with the Peano Axioms.

We define the inequalities as:

$a\leq b \iff \exists x(a+x=b)$

$a<b \iff \exists x(a+x=b) \land a\not=b$

Answer 1

Assuming we defined the natural numbers with PA

We proceed via induction on a:

Let $a = 0$:

Case 1: $b=0$:

Prove that the $0<0$ is false (fill in the details) then prove that $0 \leq 0$ is true

Case 2: $b \neq 0$:

Prove that $a \lt b$ is true then prove that $b \leq a$ is false

This is your base case, then assume that the theorem holds for some n such that $a=n$ And proceed again, using the axioms (specifically about successors) in two cases, where this time $b=a$ and $b \neq a$ (in the second case you might have to do another induction this time on b, where you start with $b = S(a) $ where $S(n) = n+1$

This is not a complete proof of course, just a sketch that might help you