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).