Zero-set inclusion for divisibility of plane polynomials

Let $p$ and $q$ be bivariate real polynomials (elements of $\mathrm{MvPolynomial}(\mathrm{Fin}\,2, \mathbb{R})$), and assume $p$ divides $q$ ($p \mid q$). Then the real plane zero set of $p$ is contained in that of $q$:

where ${Z}(p) = \{x \in \mathbb{R}^2 \mid p(x) = 0\}$ is PlaneCurveZeroSet. In words, every common real zero of the divisor polynomial is a zero of the multiple. This monotonicity lemma is used throughout the project whenever a curve is factored: it lets one replace a polynomial by any of its divisors (or pass zero-set inclusions through factorizations) when bounding intersections and singular loci.