Let $X$ be a linear space over $\mathbb{R}$. We call the mapping \begin{align*} \left\Vert \cdot \right\Vert : X\longrightarrow \mathbb{R}^+\cup \{0\} \end{align*} a norm if for all $x,y \in X$ and $t \in \mathbb{R}$ we get \begin{align*} \Vert x \Vert > 0 \Leftrightarrow x \neq {\mathbf0}, \\ \Vert t x \Vert = \vert t \vert \Vert x \Vert, \\ \Vert x + y \Vert \le \Vert x \Vert + \Vert y \Vert. \end{align*}
Is it possible to show constructively, i.e. without the use of the law of excluded middle, that \begin{align*} \Vert x \Vert = 0 \Rightarrow x = {\mathbf0}. \end{align*}
To directly answer the question: For real numbers $x$ we do have $\neg\neg(x = 0) \Rightarrow x = 0$, even though this principle is not generally intuitionistically valid, hence the classical proof which you have in mind for verifying the claim is actually intuitionistically valid.
But let me add a remark. In constructive mathematics, the expression $\mathbb{R}^+ \cup \{ 0 \}$ raises red flags. This expression denotes a particular subset of $\{ x \in \mathbb{R} \,|\, x \geq 0 \}$, consisting of those numbers which are positive or zero. With this definition of a normed space, you will have very few examples of normed spaces. For instance, not even $\mathbb{R}^1$ will be a normed space, since we can't prove constructively that the absolute value of any real number is positive or zero.
Also note that constructively there can be several distinct flavors of the reals: at least the Cauchy reals, the Dedekind reals, the MacNeille reals, the lower reals and the upper reals. You need to specify which sort of reals you are referring to. (In the first paragraph of this answer, I was referring to the Cauchy reals or the Dedekind reals.)
Lest you think that this situation seems to be complicated and off-putting, let me add that the different flavors of the reals are neatly organized: $$ \mathbb{R}_{\text{Cauchy}} \subseteq \mathbb{R}_{\text{Dedekind}} \subseteq \mathbb{R}_{\text{MacNeille}} = \mathbb{R}_{\text{lower}} \cap \mathbb{R}_{\text{upper}}. $$ They each serve a different purpose, and their differences obtain geometric meaning once interpreted in sheaf toposes. (For instance the Dedekind reals correspond to the sheaf of continuous real-valued functions, while the Cauchy reals correspond in good cases to the sheaf of locally constant real-valued functions.) Also note that, of course, there is a fully-developed intuitionistic account of metric spaces, normed spaces and their completion. The creators of this account had to think quite a bit about which kind of reals to use, how to set up the basic definitions in a sensible way and so on, but nowadays this has been settled for several decades.