The explicit antiderivative $K$ of $1/\Delta$ for Kerr, all parameter branches

Let $M,a$ be real numbers and $\Delta=r^2-2Mr+a^2$. Define $K_{M,a}:\mathbb R\to\mathbb R$ by cases on the sign of $M^2-a^2$: for $M^2>a^2$ with $b=\sqrt{M^2-a^2}$, $K(r)=\dfrac{\log\lvert r-(M+b)\rvert-\log\lvert r-(M-b)\rvert}{2b}$; for $M^2<a^2$ with $b=\sqrt{a^2-M^2}$, $K(r)=\dfrac{\arctan\big((r-M)/b\big)}{b}$; for $M^2=a^2$, $K(r)=-\dfrac1{r-M}$. Then for every $r$ with $\Delta(r)\neq0$,

Supplies the antiderivative of $1/\Delta$ used by the explicit R3 functions $H_1=M\log|\Delta|+2M^2K$ and $H_2=aK$, so that $H_1'=2Mr/\Delta$ and $H_2'=a/\Delta$ hold for every real $M,a$ (two real roots, double root, no real root).

Formalization Note Mathlib's real logarithm satisfies $\log x=\log|x|$, so the logarithmic branch is valid on both sides of each root; the case split is on $0<M^2-a^2$, $M^2-a^2<0$, else.