ThmDex – An index of mathematical definitions, results, and conjectures.
P2869
Since $x \leq y$, then two cases are possible: either $x = y$ or $x < y$. If $x = y$, then $x + z = y + z$ and thus $x + z \leq y + z$. The case $x < y$ is settled in R4227: Strict real ordering is compatible with addition. $\square$