Prove that $$f(x, y) \equiv \arccos\left(\frac{x-y}{K}\right) - \arccos\left(\frac{x-y}{K}+y\right) - \frac{y}{x}\arccos(1-y^2) \ge 0$$

with the constraints:

- $K\ge 2$ is an integer,
- $g(x, y) = (K-1)y^2+x^2-K=0$,
- $1\le x\le \sqrt{K}$,
- $0\le y\le 1$.

Furthermore, $f(x, y) = 0$ if and only if $x=y=1$ or $x=\sqrt{K}$ and $y=0$.

Numerically it seems to be correct. Also $K=2$ it can be proven.

Note that the inequality could also be replaced with $$f_2(x, y) = \arccos\left(\frac{x-y}{K}\right) - \arccos\left(\frac{x-y}{K}+y\right) - \frac{y}{x}\arccos(1-y) \ge 0$$ since $f \ge f_2$. So if $f_2 \ge 0$ then $f \ge 0$.

Blue curve is $f$ and orange one is $f_2$ when $K=3$. The $x$-axis is $x$, variable $y$ has been replace by $y = \sqrt{\frac{K-x^2}{K-1}}$.

**What I have tried:**

Setting $y = \sqrt{\frac{K-x^2}{K-1}}$ and try showing $f''_x(x, y(x)) > 0$. Numerically it is correct but the expression seems to be too complicated to prove.

Using $\arccos(a) - \arccos(b) = \int_a^b \frac{1}{\sqrt{1-z^2}}\mathrm{d}z$ to expand $f$ as the subtraction of two integrals. Then if the integrand is positive then things are proved. It works for most $z$ except for a small vicinity at $z=1$, in which the integrand is negative. Numerical test shows it is indeed the case.

Use Lagrange multiplier. $\lambda$ is easy to compute. But the second derivative seems to be too messy..

Note that when $K=2$, there is a parametrization so that $(x-y)/2 = \sin\theta$, $(x+y)/2=\cos\theta$ and $1-y^2 = \sin2\theta$ for $\theta\in [0, \pi/4]$. Therefore: $$f = \frac{\pi}{2} - \theta - \theta - \frac{y}{x} \left(\frac{\pi}{2} - 2\theta\right) = \left(1 - \frac{y}{x}\right) \left(\frac{\pi}{2} - 2\theta\right) \ge 0$$ Unfortunately, when $K > 2$, this approach seems not to work.

Note that $$\frac{x-y}{K}+y = \frac{v_0^Tv_2}{\|v_0\|\|v_2\|}$$ for $v_0 = (x, \sqrt{K-1}y)$ and $v_2 = (1, \sqrt{K-1})$, $$\frac{x-y}{K} = \frac{1}{\sqrt{K-1}}\frac{v_0^Tv_1}{\|v_1\|\|v_2\|}$$ for $v_1 = (\sqrt{K-1}, -1)$. For $K=2$ this gives a good orthogonal reference frame $(v_1, v_2)$ to solve the problem, but for $K>2$ due to the factor $1/\sqrt{K-1}$ this is not the case...