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.

But I'm not fluent enough with constructive reasoning to tell if this is a trivial or eliminable use of MCT.

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.