The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.
But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)
The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:
We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.
So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.
Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).
I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.
Best Answer
Exactly what kind of answer you get depends on the kind of proof you start with and what exactly you mean by constructive. But the proof mining approach offers an answer to some questions of this kind.
The crucial idea that comes out of it is that, to prove concrete facts, one can generally replace the notion of a prime ideal with sort of "local primality" notion. Basically, if P is a possibly prime ideal, one often doesn't need it to be truly prime to complete the proof; it might suffice, say, to look at a single pair $f_Pg_P\in P$ and need $f_P\in P$ or $g_P\in P$ to complete the argument. Therefore one can first fix the function $P\mapsto (f_P,g_P)$, and then ask for an ideal P with the property that $f_P\in P$ or $g_P\in P$. (More generally, we might hope to look at only finitely many test cases of this kind.)
At least in suitably restricted settings (say, where we are considering ideals which have reasonable finitary representations of some kind), one can extract constructive proofs along these lines.
Under suitable circumstances (in particular, one has to consider questions about how the ideal $P$ is represented) one can obtain constructive proofs this way. William Simmons I will be soon (I hope by the end of the month) uploading a paper on proof mining in polynomial and differential polynomial rings which tackles some related problems. Being polynomial rings, however, makes a big difference, because it means ideals are guaranteed to have finite representations.