Constructive Math query.

This must surely be a really simple question; but I don't yet "click"
well enough with constructive math to know the answer, so I ask.

It is a trivial theorem of orthodox math that
"any sequence which is a permutation of the harmonic sequence,
tends to zero".

Is this still provable in constructive math? The proof seems
to require looking at unbounded distances down the sequence,
so I'm not sure.

Maybe it's provable in the Russian (Markov's axiom) variant,
but just not in the minimal (Bishop) variant?

Help please.

--------------------------------------------------------------------
Bill Taylor W.Taylor@xxxxxxxxxxxxxxxxxxxxx
--------------------------------------------------------------------
Intuitionism = mathematical solipsism
--------------------------------------------------------------------

.

Loading