The sum of two nilpotent elements of a commutative ring is nilpotent. This can be done by a simple calculation using the binomial theorem.

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 (for, otherwise, the localization at $x+y$ would have a prime ideal, and this corresponds to a prime ideal in the given ring not containing $x+y$).

The general existence of prime ideals [is equivalent][1] to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra and algebraic geometry. Moreover, it can be made "constructive", well at least provable in 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][2] 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. My question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? 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 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 would be: How to come up with the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ *using* the prime ideal proof? By the latter I mean
$$V(I^n+J^n)=V(I^n) \cap V(J^n) = V(I) \cap V(J)=V(A)=\emptyset.$$
A more sophisticated example can be found [here][3], 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.
  [1]: http://mathoverflow.net/questions/98549/
  [2]: http://www.sciencedirect.com/science/article/pii/016800728390012X
  [3]: http://math.stackexchange.com/questions/919933/the-kernel-of-r-to-a-otimes-r-b-is-nil