The CReal type implements (constructive) real numbers.
Note that the comparison operations on CReal may diverge
 since it is (by necessity) impossible to implementent them
 correctly and always terminating.
This implementation is really David Lester's ERA package.