Constructive proof of univariate McCoy theorem without Dedekind-Mertens? McCoy's theorem (one of them) says that for any commutative ring $A$, $f\in A[x]$ is a zero-divisor iff it's annihilated by a scalar in $A$.
There's a widespread proof by contradiction. There's also a constructive proof using the Dedekind-Mertens lemma about polynomial content (Lombardi & Quitté p91, 2.3).
Is there a direct constructive proof that does not make use of Dedekind-Mertens, or even define content? If $fg=0$ then what is the scalar which annihilates $f$?
 A: The question you're asking might not be the question you want to ask. "What is the scalar" should be "what is the nonzero scalar", because $0$ wouldn't be interesting, right? But we don't know how to find any nonzero elements of $A$ in the first place, and they might not even exist ($A$ can be trivial). So the most natural constructive version of McCoy's theorem is actually the contrapositive statement: "If a polynomial $f \in A\left[x\right]$ has the property that the map $A \to A\left[x\right]$ that sends each scalar $r$ to $rf$ is injective, then the map $A\left[x\right] \to A\left[x\right]$ that sends each polynomial $g$ to $gf$ is also injective". If you state the theorem in this form, then the proof by contradiction that you referenced can be straightforwardly translated into an induction proof (as usual in constructivism, don't speak of "the degree" of a polynomial, but just talk about polynomials of degree $\leq k$, because you don't always know which coefficients are zero).
Now, could there be a stronger constructive version of McCoy's theorem, which would give some approximation to an "explicit zero-dividing witness", or maybe a tuple of such? I'll think about it, but let me just say that this would not be my standard interpretation of the theorem.
EDIT: Yes, there could be a stronger constructive version. But it would look somewhat awkward. It would have the following form: "Assume that $f, g \in A\left[x\right]$ are two polynomials satisfying $fg = 0$. Then, there exists a finite list $\left(u_1, u_2, \ldots, u_n\right)$ of elements of $A$ with the following two properties:
(1) Each coefficient of $g$ belongs to this list.
(2) For each $i \in \left\{1,2,\ldots,n\right\}$, if we have $u_1 = u_2 = \cdots = u_{i-1} = 0$, then $u_i f = 0$."
Such a finite list would non-constructively be a witness for the regularity (= non-zero-divisorness) of $f$, because property (1) would ensure that some $i$ satisfies $u_i \neq 0$, and then (2) would ensure that if we choose the smallest such $i$, then $u_i$ kills $f$.
For example, if $f = a + bx$ and $g = c + dx$, then $\left(bc, c, d\right)$ is such a list.
I am not sure if such a list exists in the general case, but I consider it plausible and wonder what its smallest size could be. If my hunch is right, the entries of this list are products of coefficients of $f$ and $g$, so there should be a combinatorics behind this all.
