Root count of nonzero $r : \mathrm{XCoeff}$ bounded by r.\mathrm{totalDegree

Let $r$ be a nonzero univariate coefficient polynomial, $r : \mathrm{XCoeff} = \mathrm{MvPolynomial}\,(\mathrm{Fin}\,1)\,\mathbb{R}$ with hypothesis $h_r : r \neq 0$, and let $\mathrm{CoeffRootSet}\,r$ be its set of real roots. Then the number of distinct real roots is bounded by the total degree:

This is the univariate root bound in coefficient-ring form: a nonzero polynomial over the integral domain $\mathbb{R}$ has at most $\deg r$ roots. It is the key quantitative input that turns finiteness of coefficient-root sets (e.g. roots of resultants) into explicit numerical bounds feeding the fiber-counting and pair-intersection estimates.