Normalized factor $h$ of $p$ satisfies totalDegree bound

Let $p$ and $h$ be bivariate real polynomials with $h_{p0} : p \neq 0$, and let $h_h$ witness that $h$ is one of the normalized factors of $p$ in the unique factorization monoid $\mathrm{MvPolynomial}\,(\mathrm{Fin}\,2)\,\mathbb{R}$. Then the total degree does not grow on passing to a factor:

The proof extracts $h \mid p$ from membership in the normalized factors and applies MvPolynomial.totalDegree_le_of_dvd_of_isDomain. This degree monotonicity lets the development pass global degree hypotheses on a reducible curve down to each irreducible factor, so that the per-pair bound of irreducible_pair_intersection_bound, namely $(d_1 + d_2 + 1)^4$, applies to every factor pair and can be summed in factorized_bezout_bound; it is used the same way in factor_intersection_bound.