Derivative with a simple pole forces regularity

Throughout, $K$ is a field of characteristic zero with a derivation $D$, and $K(X)$ is the field of rational functions in one variable over $K$, equipped with a derivation (also written $D$) that extends the derivation of $K$. Let $p\in K[X]$ be an irreducible polynomial and put $Dp=q$ with $q\in K[X]$ (the derivative of a polynomial is a polynomial), and assume $p\nmid q$. Let $x\in K(X)$ and suppose the derivative $Dx$ has at most a simple pole at $p$, i.e. $Dx = r/(p\,s)$ for some polynomials $r,s$ with $p\nmid s$. Then $x$ has no pole at $p$: there are polynomials $a,b$ with $p\nmid b$ and $x=a/b$.

This is the local statement behind the fact that in the logarithmic derivative of a rational function, all poles are simple: a function with a pole of order $m\ge1$ at a prime $p$ not dividing its own derivative has a derivative with a pole of order exactly $m+1$.

Formalization Note The hypothesis hpoly states that the derivative of every polynomial is again a polynomial; the conclusion is phrased as $x\cdot b=a$ in $K(X)$.