to use this object to model arithmetic infinity. For instance,
depending on implementation details, it might happen that `leq n ξ` is
true for all (finite) natural numbers `n`. However, the fixed point
to use this object to model arithmetic infinity. For instance,
depending on implementation details, it might happen that `leq n ξ` is
true for all (finite) natural numbers `n`. However, the fixed point