Coprime primitive curries never specialize both to zero

Let $p$ and $q$ be bivariate real polynomials, let $x : \mathbb{R}$ be a coefficient coordinate, and assume the curried forms are relatively prime, $h_{rel} : \mathrm{IsRelPrime}\,(\mathrm{Curry0}\,p)\,(\mathrm{Curry0}\,q)$. The statement also carries primitivity hypotheses on the curries (binders _hpprim $: (\mathrm{Curry0}\,p).\mathrm{IsPrimitive}$ and _hqprim $: (\mathrm{Curry0}\,q).\mathrm{IsPrimitive}$); they are present in the statement but not used by the proof. Then the two specialized univariate polynomials at $x$ do not both vanish:

The proof shows that if both specializations vanished, the line factor $\mathrm{CoeffLineFactor}\,x$ would divide both $p$ and $q$, hence its curry would divide both curries and would be a unit by $h_{rel}$; but that factor has a nonzero coefficient of positive degree, so it is not a unit. In the resultant/fiber-counting argument this guarantees that, over each coefficient value $x$, the common zeros are roots of a nonzero univariate polynomial.