Solution (source code)

= Solution

For a positive remaining <fraction> $n/d$, the condition $1/q\leq n/d$ is equivalent to $q\geq d/n$. Since $1/q$ decreases as the positive <integer> $q$ increases, \b[choose $q=\lceil d/n\rceil$]. The zero <fraction> needs no term. This is the <greedy Egyptian fraction expansion>.

The remaining <fraction> is
$$
\frac nd-\frac1q=\frac{nq-d}{dq}.
$$
The defining inequalities $q-1<d/n\leq q$ give $0\leq nq-d<n$. Therefore the unreduced new numerator is a nonnegative <integer> strictly smaller than the old positive numerator. Passing to a <reduced fraction> can only reduce it further. That numerator is a <loop variant>, so the process terminates. The increasing denominators are not the termination argument; their size need not be bounded in advance.