A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where applicable, lemmas that will be reused in other contexts have been stated in extra generality.
There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology. This is a concrete implementation that is useful for simplicity and computability reasons.
sequence, cauchy, abs val, absolute value
A function f is an absolute value if it is nonnegative, zero only at 0, additive, and multiplicative.
A sequence is Cauchy if the distance between its entries tends to zero.
The constant Cauchy sequence.
lim_zero f holds when f approaches 0.
The entries of a positive Cauchy sequence eventually have a positive lower bound.