Intersection bound for an irreducible curve with a partial-derivative factor

Let $h$ be an irreducible plane polynomial ($h_h$) of total degree at most $d$, with a nonzero partial derivative $h_{pi} : \mathrm{pderiv}\,i\,h \ne 0$ for some $i : \mathrm{Fin}\,2$, and let $k$ be a normalized factor of that partial derivative ($h_k : k \in \mathrm{normalizedFactors}\,(\mathrm{pderiv}\,i\,h)$) that is not associated to $h$ ($h_{\mathrm{not}} : \neg\,\mathrm{Associated}\,h\,k$). Then the intersection of the two real zero sets is finite with an explicit bound:

The factor $k$ is irreducible with total degree at most $d$ (via normalized_factor_degree_le and totalDegree_pderiv_le), and the proof is the same three-way case split as in irreducible_pair_intersection_bound: both curries of degree zero (empty intersection), exactly one of degree zero (bound $d \cdot d$), or both positive (primitive coprime curries, bound $((d+d)^2+1) \cdot d$); each is at most $(d+1)^4$. The associated case is excluded by $h_{\mathrm{not}}$, which partial_factor_not_associated supplies in the application. Every singular point of $h$ lies in at least one such intersection $Z(h) \cap Z(k)$ (singularPointSet_subset_partial_factor_union), so this lemma is the per-factor input to the finiteness and bound for the singular locus in finite_singularities_of_irreducible_bound.