Sorry, this is not an answer, but rather a too-long elaboration on constructive aspects. I post this here because there was some interest about the constructive content of the theorem in the comments.

1. As pointed out in the comments, the first thing to get straight is the definition of a Noetherian module (or ring). For instance, with the usual definition "any submodule is finitely generated", even the $\mathbb{Z}$-module $\mathbb{Z}$ cannot be shown to be Noetherian constructively: Pick a formula $\varphi$ such that neither $\varphi$ nor $\neg\varphi$ can be shown. Then consider the submodule $U = \{ x \in \mathbb{Z} \,|\, (x = 0) \vee \varphi \}$. If $U$ were finitely generated, it would a forteriori be generated by a single element (Euclid's algorithm) and we could decide whether $1 \in U$ or $1 \not\in U$, that is whether $\varphi$ or $\neg\varphi$.

2. A suitable notion of a Noetherian module is given in the very fine book *A Course in Constructive Algebra* by Mines, Richman, and Ruitenburg: A module is Noetherian if every ascending chain of finitely generated submodules stops (think "$U_n = U_{n+1}$", not "$U_n = U_{n+1} = U_{n+2} = \cdots$").

 This definition works fine for many purposes, but not for showing that $R[X]$ is Noetherian if $R$ is. See Chapter VIII of that book. Also it doesn't work well if dependent choice is not available, since it refers to *sequences*, which can be quite elusive without choice.

 A different definition appears in http://www.mittag-leffler.se/sites/default/files/IML-0001-30.pdf (by Coquand and Lombardi). There they claim that Noetherianity of $R$ implies Noetherianity of $R[X]$.

 Finally let me recommend the nice article *Strongly Noetherian rings and constructive ideal theory* by Hervé Perdry. He surveys several kinds of Noetherian conditions.

3. A thesis of Coquand, Lombardi and others is that the Noetherian condition is often not the right one constructively. Instead, one should refer to the notion of a *coherent ring*. In classical mathematics, any Noetherian ring is coherent. See for instance page 27 of *Commutative Algebra: Constructive Methods* by Lombardi and Quitté.

4. Finally, a short and constructive proof that the Krull dimension of $K[X_1,\ldots,X_n]$ is $n$ appears at http://hlombardi.free.fr/publis/KrullMathMonth.pdf (by Coquand and Lombardi).