Monotonic and bounded sequences throughout mathematics When I refer to the Monotone Convergence Theorem below, I refer to the very simple claim that if a non-decreasing sequence has an upper bound then it converges. I don't refer to the claim from Measure Theory.
One application I know of for this theorem is to recurrence relations. One shows that a recurrence relation like $a_{n+1} = \sqrt{2 + a_n}, a_0 = 0$ is non-decreasing and bounded, from which one concludes that it has a limit as $n$ approaches $\infty$.
Are there any other applications of the theorem?
I ask because I'm curious about the possibility of systematically "constructivising" applications of this theorem. Obviously in general this isn't possible. But surely there are lots of situations in which it may be possible.
I tried constructivising Herschfeld's Convergence Theorem, I believe successfully. The resulting argument is a great deal less straightforward than Herschfeld's original one.
[edit]
There was a slight misunderstanding in the comments. The Cauchy completeness of the real numbers does not imply the Monotone Convergence Theorem, unless one assumes the Law of Excluded Middle.
 A: I am going to speak in intuitionistic mathematics here, as that's what's relevant for this question.
It's worthwhile recalling a bit of background.
There are several notions of completeness of an ordered field:


*

*Cauchy completeness: every Cauchy sequence converges.

*Dedekind completeness: every Dedekind cut determines an element of the field.

*MacNeille completeness: an inhabited bounded set has a supremum.


The field of rationals may be completeted with respect to any one of these to yield three kinds of reals, the Cauchy reals $\mathbb{R}_C$, the Dedekind reals $\mathbb{R}_D$ and the MacNeille reals $\mathbb{R}_M$. These are related as $\mathbb{R}_C \subset \mathbb{R}_D \subset \mathbb{R}_M$.
The principle "a bounded non-decreasing sequence has a supremum" holds in $\mathbb{R}_M$, but it cannot be shown to hold in $\mathbb{R}_D$ (and even less so in $\mathbb{R}_C$). 
The principle does not fail completely for $\mathbb{R}_D$. If $a : \mathbb{N} \to \mathbb{R}_D$ is a non-decreasing sequences, we can define the lower Dedekind cut $L = \{q \in \mathbb{Q} \mid \exists n . q < a_n\}$, but not in general the upper cut. Thus, the supremum $\sup_n a_n$ exists as a lower Dedekind real, which is good enough in some situations.
Many uses of the principle are inessential, especially when with some extra effort we can show that the non-decreasing sequence is Cauchy (I imagine this is what you did to prove Herschfeld's Convergence Theorem). For an essential use, we need to look for applications in which the non-decreasing sequence cannot be shown to be Cauchy. This often happens when the sequence depends on some extra parameters. Let me give one such simple example.
Consider the sequence of functions $f_n : [0,1] \to \mathbb{R}$ where $f_n(x) = x^n$. Using the principle "every bounded non-increasing sequence has an infimum", we can show that $(f_n)_n$ converges point-wise on $[0,1]$. Indeed, given any $x \in [0,1]$, it is easy to see that $x \geq x^2 \geq x^3 \geq \cdots$, therefore $\lim_n f_n(x)$ exists. Of course, the limit map $f(x) = \lim_n x^n$ satisfies $f(1) = 1$ and $f(x) = 0$ for $x \in [0,1)$. Without the principle, we cannot show that $(f_n)_n$ converges pointwise because its limit $f$ would be a discontinuous function.
Incidentally, the above example shows that there are discontinuous maps on MacNeille reals.
A: I'm not sure if this is an answer to your question but it seems like it might be.  In enumerative combinatorics one often has a sequence of nonnegative integers $(a_n)$ and wants to estimate its growth rate.  A standard way to proceed is to form the generating function $\sum_n a_n x^n$ or $\sum_n a_n x^n\!/n!$ and then show that it converges to an analytic function.  Then one can apply methods from complex analysis.  The proof of convergence focuses on showing that the sequence $(a_n)$ doesn't grow too fast; one basically takes for granted that this means that the series converges (at least pointwise), because of what you're calling the Monotone Convergence Theorem.
There are lots of examples in the book Analytic Combinatorics by Flajolet and Sedgwick.
But I'm not fluent enough with constructive reasoning to tell if this is a trivial or eliminable use of MCT.
