Interesting that for Cauchy sequences in question they necessarily have to be non-constructive, i.e. one can't name any element in the sequence. Edit: oops, no

Interesting that for Cauchy sequences in question they necessarily have to be non-constructive, i.e. one can't name any element in the sequence. Edit: oops, not that. The sequence itself - not the "useful reals" element of the sequence - has to be non-constructive...