For $\alpha >0$ every ordinal $\beta$ is $\alpha \cdot \xi +\rho$ with $\rho <\alpha$, in exactly one way

Let $\alpha$ and $\beta$ be ordinals (Ordinal (von Neumann)) with $\alpha >0$. Then there are unique ordinals $\xi$ and $\rho$ with

$\beta =\alpha \cdot \xi +\rho \text{and}\rho <\alpha \mathrm{.}$

$\xi$ is the quotient and $\rho$ the remainder of $\beta$ on division by $\alpha$; concretely, $\xi$ is the largest ordinal with $\alpha \cdot \xi \le \beta$, and $\rho$ is what For $\alpha \le \beta$ there is exactly one ordinal $\gamma$ with $\alpha +\gamma =\beta$ returns from $\alpha \cdot \xi \le \beta$.

No choice principle is used.

Why the least $\eta$ with $\beta <\alpha \cdot \eta$ has to be a successor. Because $\eta \mapsto \alpha \cdot \eta$ is continuous at limits: at a limit stage its value is the supremum of the earlier values, so it cannot overtake $\beta$ for the first time there. That is claim (f) 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$ in the form used at step 4.1, and it is the only place the limit clause of Ordinal multiplication $\alpha \cdot \beta$ is used.

The bound $({\beta }^{+}{)}^{+}$ is a Separation device. "The least $\eta$ with $\beta <\alpha \eta$" quantifies over all ordinals, which is not a set; step 1.1 supplies a specific witness inside $({\beta }^{+}{)}^{+}$, so the collection can be cut out of a set. Nothing depends on the particular bound.

Uniqueness is proved before existence, and independently of it. Step 1.2 uses only the monotonicity laws, so it applies to any two representations whatever their origin. This is the order used again in 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, where uniqueness is what licenses the definite article in "the Cantor normal form".

The remainder can be $0$ and the quotient can be $0$. If $\beta <\alpha$ then $\xi =0$ and $\rho =\beta$; if $\alpha$ divides $\beta$ exactly then $\rho =0$. Neither case is excluded, and neither needs separate treatment.