I want to prove the following construction of a function over the Poincaré disk is not an isometry. Let $X$ the Poincaré disk and $\partial X$ the boundary of $X.$ For $a \in \partial X$ (a point at "infinity") and a positive number $\varepsilon$ we considerer $f_{a,\varepsilon} \colon X \to X$ as follows: $p \mapsto f_{a,\varepsilon}(p)$ where $f_{a,\varepsilon}(p)$ is such that we move to the "right" over the horocycle that contains $p$ and $a.$
My claims is the previous function is not an isometry, because the length of an arc of a horocycle between two points is longer than the length of the line segment between those two points. But I am not able to prove my claim. If you dont understand the function maybe with the following draw it will be clear.
In the previous image $H_p$ is the horocycle that contains $a$ and $p.$ Then I want prove the hyperbolic distance between $p$ and $q$ is different than the hyperbolic distance between $f_{a,\varepsilon}(p)$ and $f_{a,\varepsilon}(q).$
I presume, from the picture and the notation, that the distance along the horocycle that one moves when going from $p$ to $f_{a,\epsilon}(p)$ is equal to $\epsilon$.
To prove that $f_{a,\epsilon}$ is not an isometry, it would be easiest to work in the upper half plane model using $a=\infty$, in which the horocycles are the horizontal lines $y=y_0$ along which the horocyclic distance is $\Delta x / y_0$. We may take $p = (0,1)$ and so $H_p$ is the $y=1$ horocycle. Take $q=(0,y_0)$, and so $H_q$ is the $y=y_0$ horocycle, where $y_0 \ne 1$. We have $d(p,q) = \ln|y_0|$, and $A = f_{a,\epsilon}(p) = (\epsilon,1)$, and $B = f_{a,\epsilon}(q) = (\epsilon y_0,y_0)$.
Every distance mimizing line segment from the $y=1$ horocycle $H_p$ to the $y=y_0$ horocycle $H_q$ is a "vertical" line segment in the upper half plane, from a point $(x,1)$ to the point $(x,y_0)$, all having the same length $\ln|y_0|$. Every "nonvertical" path from a point on $H_p$ to a point on $H_q$ has length strictly larger than $\ln|y_0|$. Since the points $A$ and $B$ do not lie on the same vertical segment (because $\epsilon \ne \epsilon y_0$), every path between those two points $A,B$ has length strictly larger than $\ln|y_0|$; its not hard to prove this by simply looking at the path length integral for any parameterized path from $A$ to $B$, and using the fact that the path must have a nonvertical tangent line along a subinterval of the parameter interval. It follows that $f_{a,\epsilon}$ is not an isometry.