For $\alpha \le \beta$ there is exactly one ordinal $\gamma$ with $\alpha +\gamma =\beta$

Let $\alpha$ and $\beta$ be ordinals (Ordinal (von Neumann)) with $\alpha \le \beta$. Then there is exactly one ordinal $\gamma$ with

$\alpha +\gamma =\beta ,$

namely the order type of the set $\beta \setminus \alpha$ of ordinals lying in $\beta$ but not in $\alpha$, taken with the membership order (Every well-order has a unique order type).

This is subtraction on the left: the unknown sits on the right of the $+$ sign, which is the side on which ordinal addition is strictly increasing and cancellative (Monotonicity of ordinal $+$ and $\cdot$: strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities $0+\beta =\beta$ and $1\cdot \beta =\beta$). Subtraction on the other side does not exist in general: there is no ordinal $\gamma$ at all with $\gamma +\omega =\omega +1$, since $\gamma +\omega$ is a limit ordinal for every $\gamma$ while $\omega +1$ is a successor.

No choice principle is used.

The proof is a picture. $\beta$ is a copy of $\alpha$ followed by whatever is left, and "whatever is left" is $\beta \setminus \alpha$. Clause (b) of $\alpha +\beta$ is the order type of $\alpha$ followed by $\beta$ says exactly that the order type of a well-order split at an initial segment is the sum of the two order types, so no recursion is needed at all.

Why the hypothesis $\alpha \le \beta$ cannot be dropped. $\alpha \le \alpha +\gamma$ always holds (claim (b) of Monotonicity of ordinal $+$ and $\cdot$: strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities $0+\beta =\beta$ and $1\cdot \beta =\beta$), so $\alpha +\gamma =\beta$ forces $\alpha \le \beta$. The theorem is therefore sharp: the equation is solvable exactly when the hypothesis holds.

The other-sided equation. The claim in the Statement that no $\gamma$ satisfies $\gamma +\omega =\omega +1$ uses only that $\gamma +\omega$ is a limit ordinal, which is claim (g) of Monotonicity of ordinal $+$ and $\cdot$: strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities $0+\beta =\beta$ and $1\cdot \beta =\beta$, and that $\omega +1={\omega }^{+}$ is a successor. Right subtraction, when it exists, is also not unique: $0+\omega =1+\omega =\omega$, so the equation $\gamma +\omega =\omega$ has at least two solutions (FALSE: $\beta <\gamma$ implies $\beta +\alpha <\gamma +\alpha$).

Where it is used. Existence of the remainder in For $\alpha >0$ every ordinal $\beta$ is $\alpha \cdot \xi +\rho$ with $\rho <\alpha$, in exactly one way is a direct application, and that theorem in turn is what extracts the coefficients of a Cantor normal form (Cantor normal form: every nonzero ordinal is ${\omega }^{{\beta }_0}\cdot c_0+\cdots +{\omega }^{{\beta }_{k-1}}\cdot c_{k-1}$ with ${\beta }_0>\cdots >{\beta }_{k-1}$ and each $c_i$ a nonzero natural number, in exactly one way).