Given the definition of $\leq$, prove $((a \leq b) \implies (b \leq a)) \implies (a = b)$.

Question

Given the definition of $\leq$, prove $((a \leq b) \implies (b \leq a)) \implies (a = b)$.

$\leq$ is defined as:
$a \leq$ b :=
Case $a=0: True$
Case $a=Succ(p)$:
....Case $b=0: False$
....Case $b=Succ(q): p \leq q$

(*Succ(n) means the successor of n which is (n+1))

Prove $((a \leq b) \implies (b \leq a)) \implies (a = b)$

Answer 1

By reductio ad absurdum: supose $\;a\neq b\;$ and without resticting generality, supose $\;a<b\;$ . But then $\;b\rlap{\,\;/}< a\;$ ,which contradicts the premise.

Or using the usual definition of inequality:

$$a<b\implies b-a>0\implies a-b=-(b-a)<0\implies b\rlap{\;\,/}<a\;\;\text{-- contradiction}$$