For a proof, I need to use the fact that if an integer, say $x$ is bounded on both sides by another integer $y$, then $x = y$.
Is this something that needs to be proven, or is this part of the definition of equality of two integers? My gut instinct says it is the latter, but I would like a source if possible as I cannot find one.
A possible (semi-formal) proof.
We have that : $y \le x \le y$ is ; $(y \le x) \text { and } (x \le y)$.
But $(x \le y)$ means : $(x < y) \text { or } (x=y)$.
And $(y \le x)$ means : $(y < x) \text { or } (y=x)$.
Four cases : (1) $(x < y)$ and $(y < x)$ : contradiction. The same for (2) $(x < y)$ and $(y = x)$ and (3) $(y < x)$ and $(x=y)$.
Why contradiction ? Because $x < y$ is defined as : $y=k+x$ for some $k \ne 0$.
Thus, we are left with :
Alternatively, we may start defining directly $x \le y$ as : $y=k+x$, where in this case $k$ may be $0$.
Thus, from $(x \le y)$ and $(y \le x)$ we have : $y=k+x$ and $x=l+y$.
Now, using property of $=$, we have :
But this holds only if $k=l=0$.
Thus, we have $y=k+x=0+x=x$.