There are a couple of very similar statements that all work out:

1. if $x$ and $y$ are both apart from $0$, then $xy$ is apart from $0$.
2. If $x$ is apart from $y$ and $xy = 0$, then $x = 0$ or $y = 0$ (as mentioned by Andreas Blass in the comments).
3. $xy = 0$ iff $\min \{|x|,|y|\} = 0$.

A more round-about way which works at least in computable analysis even allows to make case distinctions here. (Classical metatheory from here on). We can use the three-valued space $\mathbb{T}$ with underlying set $\{\bot,0,1\}$ and topology generated by $\{\{0\},\{1\}\}$. Given $x,y \in \mathbb{R}$ with $xy = 0$, we can compute $c(x,y) \in \mathbb{T}$ where $c(x,y) = 0$ if $y \neq 0$, $c(x,y) = 1$ if $x \neq 0$ and $c(0,0) = \bot$.

For any reasonable[1] space $\mathbf{X}$, the map $\operatorname{Merge}_\mathbf{X} : \subseteq \mathbb{T} \times \mathbf{X} \times \mathbf{X} \to \mathbf{X}$ defined as $\operatorname{Merge}_\mathbf{X}(0,x,y) = x$, $\operatorname{Merge}_\mathbf{X}(1,x,y) = y$ and $\operatorname{Merge}_\mathbf{X}(\bot,x,x) = x$ will be computable. Note that $\operatorname{Merge}_\mathbf{X}(\bot,x,y)$ is undefined if $x \neq y$.

Thus, we are allowed to make a case distinction according to the zero product property in computable analysis, as long as we end up with the same result no matter which case we pick if they are both true (and as long as the result lives in a reasonable[1] space). This is not really specific to the zero product property, but more a general case of being able to get away with something that may at first glance look like using $\mathrm{LLPO}$.

[1] Reasonable spaces include the computably admissible ones, as well as any other example I'm aware of anyone would want to be working with. It doesn't work for everything though.

There are a couple of very similar statements that all work out:

1. if $x$ and $y$ are both apart from $0$, then $xy$ is apart from $0$.
2. If $x$ is apart from $y$ and $xy = 0$, then $x = 0$ or $y = 0$ (as mentioned by Andreas Blass in the comments).
3. $xy = 0$ iff $\inf \{|x|,|y|\} = 0$.

A more round-about way which works at least in computable analysis even allows to make case distinctions here. (Classical metatheory from here on). We can use the three-valued space $\mathbb{T}$ with underlying set $\{\bot,0,1\}$ and topology generated by $\{\{0\},\{1\}\}$. Given $x,y \in \mathbb{R}$ with $xy = 0$, we can compute $c(x,y) \in \mathbb{T}$ where $c(x,y) = 0$ if $y \neq 0$, $c(x,y) = 1$ if $x \neq 0$ and $c(0,0) = \bot$.

For any reasonable[1] space $\mathbf{X}$, the map $\operatorname{Merge}_\mathbf{X} : \subseteq \mathbb{T} \times \mathbf{X} \times \mathbf{X} \to \mathbf{X}$ defined as $\operatorname{Merge}_\mathbf{X}(0,x,y) = x$, $\operatorname{Merge}_\mathbf{X}(1,x,y) = y$ and $\operatorname{Merge}_\mathbf{X}(\bot,x,x) = x$ will be computable. Note that $\operatorname{Merge}_\mathbf{X}(\bot,x,y)$ is undefined if $x \neq y$.

Thus, we are allowed to make a case distinction according to the zero product property in computable analysis, as long as we end up with the same result no matter which case we pick if they are both true (and as long as the result lives in a reasonable[1] space). This is not really specific to the zero product property, but more a general case of being able to get away with something that may at first glance look like using $\mathrm{LLPO}$.

[1] Reasonable spaces include the computably admissible ones, as well as any other example I'm aware of anyone would want to be working with. It doesn't work for everything though.