Ordinal division algorithm (source code)

= Ordinal division algorithm
{title2=$\alpha=\delta q+r,\quad r<\delta$}

For <ordinals> $\alpha$ and $\delta>0$, there are unique ordinals $q,r$ with the displayed relation. The function $q\mapsto\delta q$ is strictly increasing, continuous at limit ordinals and unbounded. Its first value above $\alpha$ occurs at a successor, giving the largest $q$ with $\delta q\le\alpha$. The ordered tail of $\alpha$ after that initial segment gives $r$, and maximality gives $r<\delta$.