Prove $(1-\frac{8}{\pi^2})x^2\cot^2(x)+\frac{8}{\pi^2}x\cot(x)+\frac{4}{\pi^2}x^2-1\ge0$ for $x\in[0,\pi/2]$ 
How to prove the following inequality:
$$\left(1-\frac{8}{\pi^2}\right)x^2\cot^2(x)+\frac{8}{\pi^2}x\cot(x)+\frac{4}{\pi^2}x^2-1\ge0,\quad x\in[0,\pi/2]?$$

I evaluated the LHS of the above inequality numerically. I found that equality holds at $x=0$ and $x=\pi/2$, and strict inequality holds elsewhere. The LHS is not a monotonic function; as $x$ increases it first increases and then decreases. I derived the derivative of the LHS and the results are quite messy. Is there any easier ways of proving the inequality?
 A: A partial answer - I am going to show that the given inequality holds for every $x\in(0,1]$.
Since the cotangent is the logarithmic derivative of the sine function we have
$$ \cot x = \frac{1}{x} + \sum_{n\geq 1}\left(\frac{1}{x-n\pi}+\frac{1}{x+n\pi}\right) \tag{1} $$
and
$$ \frac{1-\pi z\cot(\pi z)}{2} = \sum_{n\geq 1}\zeta(2n) z^{2n}.\tag{2} $$
This gives the Taylor series of $z^2\cot(z)^2$ too, and allow us to state that the given LHS is
$$ \left(-\frac{2}{3}+\frac{20}{3 \pi ^2}\right) x^2+\left(\frac{1}{15}-\frac{32}{45 \pi ^2}\right) x^4+\sum_{k\geq 3}c_k x^{2k},\qquad c_k\geq 0\tag{3} $$
for any $x\in\left(0,\frac{\pi}{2}\right)$, so the given inequality holds over the interval $\left(0,1\right]$ for sure.
That should be most of the job.

The given inequality is indeed equivalent to
$$\forall x\in\left(0,\frac{\pi}{2}\right),\quad x\cot(x)\geq \frac{-4+\sqrt{\left(\pi ^2-4\right)^2-4 \left(\pi ^2-8\right) x^2}}{\pi ^2-8} $$
where the RHS is a remarkably good approximation of the LHS.
The (generalized) Shafer-Fink inequality should completely settle the question, but I have to perform some numerical experiments. In a Shafer-Fink-suitable form, the previous line can be written as
$$ \forall x>0,\quad \frac{\arctan x}{x}\geq \frac{-4+\sqrt{\left(\pi^2-4\right)^2+4 \pi ^2 x^2}}{\pi^2-8+4 x^2}\tag{4} $$
A: Regarding Jack's inequality (4), I'd like to post some numerical results
The LHS is given by the red curve, and the RHS of (4) in Jack's answer shown by the black dashed curve. We see that these two curves are almost indistinguishable! The (generalized) Shafer-Fink inequality in Jack's paper (Theorem 1, I haven't checked other inequalities) would give us the blue curve, which is looser than the RHS.
This is actually a very cool inequality. A proof would be quite interesting.
