It is said that proofs in constructive math, if possible at all, tend to be more verbose than in classical math. I'm trying to get an intuition for this, so:
Are there any good example of theorems mathematicians use, for which the proof in constructive math is considerably larger that the proof in classical math?
I'm not looking for artificial examples like in this question (https://mathoverflow.net/questions/294092/g%c3%b6dels-speed-up-from-constructive-to-classical-logic), but rather for meaningful theorems.
The proof that there are irrational numbers $a$, and $b$ such that $a^b$ is rational using $a = \sqrt{2}^\sqrt{2}$ and $b = \sqrt{2}$ is a good example. I believe it has a constructive proof that that is fairly long but the classical proof is short. However that's also a good case for showing that it need not always be that way, since there's a constructive proof that is almost as short as the non-constructive proof using $a = \sqrt{2}$ and $b = \log_2{9}$.