Corollary

— In an ordered group $G$, the relations $x \leq y$, $0 \leq y - x$, $x - y \leq 0$ and $-y \leq -x$ are equivalent.

In fact, we apply Prop. 2, successively taking $z = -x$, $z = -y$ and $z = -(x + y)$.

In particular we deduce from this corollary that if $G$ is an ordered group, the map $x \mapsto -x$ from $G$ to itself takes the ordering of $G$ to the opposite ordering.