Positive-degree partial drops total degree by at least one

Let $h$ be a bivariate real polynomial, $i : \mathrm{Fin}\,2$ a variable index, and assume $h$ has positive total degree (binder _hpos $: 0 < h.\mathrm{totalDegree}$). Then the partial derivative has total degree at most one less:

with truncated natural-number subtraction. The positivity hypothesis appears in the statement but is not used by the proof, which works monomial by monomial: differentiating a monomial with exponent vector $v$ either kills it (if $v_i = 0$) or lowers the exponent sum by exactly one. The lemma is used in totalDegree_pderiv_le (the positive-degree branch) and in totalDegree_pderiv_lt_of_nonzero, which in turn supports irreducible_not_dvd_nonzero_partial in the singularity analysis.