Recall the well-known proof that a unique factorization domain is a GCD domain:
Let $x, y \in R \setminus \{ 0 \}$. Factor $x$ and $y$ into pairwise non-associated irreducible elements: $$\begin{align*}x &= p_1^{e_1} \cdots p_n^{e_n}, \\ y &= p_1^{f_1} \cdots p_n^{f_n}.\end{align*} $$ Then one can check that the product $p_1^{r_1} \cdots p_n^{r_n}$ with $r_i := \min\{ e_i, f_i \}$ is a greatest common divisor of $x$ and $y$.
Here, a unique factorization domain is an integral domain such that every nonzero element admits a factorization into irreducible elements which is unique up to reordering and associatedness, and a GCD domain is an integral domain such that there exists a greatest common divisor for any two elements.
Constructively, the problem with the above proof is that we may not be able to decide for given irreducible elements whether they are associated or not. Using the given (classically standard) definitions, I thus do not see that the implication $$\text{$R$ is a unique factorization domain} \Longrightarrow \text{$R$ is a GCD domain}$$ is constructively provable.
Question. Is there an elegant constructive notion of unique factorization domain such that the implication does hold constructively?
Remark 1. Note that in unique factorization domains which happen to be GCD domains, associatedness and even divisibility are indeed decidable: Given elements $x$ and $y$, consider a gcd $d$ of $x$ and $y$. Write $x = ds$. Then $x|y$ iff $s$ is invertible. This is the case iff the number of factors in a factorization of $s$ into irreducible elements is zero. Because the natural numbers are discrete, this can be decided.
Remark 2. In Mines, Richman, Ruitenburg: A Course in Constructive Algebra approximately the same definitions are used and the implication is stated without proof (see theorem IV.2.3 on page 114). Richman wrote elsewhere (section 6) that he considers the treatment of unique factorization domains in this book to be incomplete.
