Add an availability paragraph to the conclusion.
A minor wording change in the explanation of wellorder_def.
Add a simple theorem (lt_omega) to the discussion of limits.