Proof that the greedy algorithm for Egyptian fractions terminates

We wish to prove that the following greedy algorithm, which represents any fraction x=a/b between 0 and 1 as a sum of reciprocals, always terminates:

1. If x=0, terminate.
2. Else, let n=ceil(1/x).
3. Output 1/n.
4. Let x=x-1/n.
5. Repeat.

When x=a/b, we output some n satisfying each of the following:

  1/n <= a/b < 1/(n-1)
  n   >= b/a > n-1
  an  >= b  > an-a
  an-b >= 0 > (an-b) - a

After subtracting 1/n, we're left with (an-b)/(bn). But we know that an-b < a, so even before cancellation the numerator of our fraction decreases. Cancellation can only lower the numerator further. Hence printing a/b will take at most a reciprocals.