Membership characterization of coefficient-line zero sets

Let $a$ be a univariate coefficient polynomial in $\mathrm{MvPolynomial}\,(\mathrm{Fin}\,1)\,\mathbb{R}$ and $p$ a plane point ($\mathrm{Point2}$). Then membership $p \in \mathrm{CoeffLineZeroSet}\,a$ holds exactly when $a$ vanishes at the coefficient coordinate $p\,1$,

and the two conditions coincide by definitional unfolding (Iff.rfl).

In geometric terms, $\mathrm{CoeffLineZeroSet}\,a$ is the set of points whose coefficient coordinate $p\,1$ is a real root of $a$, that is, a union of lines of constant coefficient coordinate, one for each real root. This simp lemma is used to unfold line--curve intersections into root conditions on fibers.