How do working constructivists get by with out the zero product property?

Question

It is stated by Douglas Bridges in Constructive mathematics: a foundation for computable analysis that the following property, which I will call the zero product property:

If $x,y \in \mathbb{R}$ and $xy = 0$, then $x = 0$ or $y = 0$.

is equivalent to the Lesser Limited Principle of Omniscience (LLPO):

For each binary sequence $(a_n)$ with at most one term equal to 1, either $a_{2n} = 0$ for all $n$ or else $a_{2n+1} = 0$ for all $n$.

The LLOP is non-algorithmic and a trivial consequence of the Law of Excluded Middle (LEM); as such it is often rejected by constructive mathematicians. In light of this revelation how do construcivists operate, in general situations, without use of the zero product property?

Edit: The following example is referenced in some of the answers below but has been removed from the original post because it is receiving more attention than the fundamental question.

$$x^2-4 = 0 \implies (x-2)(x+2) = 0 \implies x-2 = 0 \ \text{or} \ x+2 = 0 \implies x = 2 \ \text{or} \ x = -2.$$

I realize the example given is fairly easy to reconcile without the zero product property. I'm looking for answers that give more general techniques employed to operate with out the zero product property. I've gathered that typically one must add extra assumptions (e.g. apartness of x and y.)

Answer 1

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.