Prove that $$ \sum \limits_{k=1}^{2n+1} (-1)^{k+1} \: \text{arccot} F_{2k-1} > \text{arccot} \: 2$$ holds for all $n \in \mathbb{N}$.
(The Fibonacci sequence, defined by the recurrence $F_1 = F_2 = 1$ and $\forall n \in \mathbb{N},$ $F_{n+2} = F_{n+1} + F_n$)
My work. I proved that the sequence $a_n=\sum \limits_{k=1}^{2n+1} (-1)^{k+1} \: \text{arccot} F_{2k-1}$ is decreasing. Therefore inequality cannot be proved by induction.
Show that
$$\text{arccot} F_{2n+1} = \text{arccot} L_{2n} + \text{arccot} L_{2n+2}, \quad (1)$$ where $L_n$ is the Lucas series with $L_0 = 2, L_1 = 1 , L_3 = 3, L_{n+2} = L_{n+1} + L_n$.
Hence,
$$ \sum \limits_{k=1}^{2n+1} (-1)^{k+1} \: \text{arccot} F_{2k-1} = \text{arccot} L_0 + \text{arccot} L_{4n+2} > \text{arccot} 2 $$
Proof of (1):
A necessary condition for integer solutions to $\tan^{-1} \frac{1}{x} = \tan^{-1} \frac{1}{y} + \tan^{-1} \frac{1}{z}$ is $ 1/x = \frac{ 1/y + 1/z} { 1 + 1/(yz)}$, or that $1+yz = xy+xz \Rightarrow (y-x)(z-x) = x^2 - 1$.
So, with $L_n = F_{n-1} + F_{n+1}$, we can verify that
$(L_{2n} - F_{2n+1} ) ( L_{2n+2} - F_{2n+1} ) = F_{2n-1} F_{2n+3} = F_{2n+1} ^2 - (-1)^{2n+1} = F_{2n+1} ^2 + 1$
Finally, show that this is a sufficient condition because the angles are small enough.
To de-construct what I did, I stumbled upon the observation that the cotangent of the difference was an integer, and started to hunt down what it was. Having the Lucas number $L_{4n+2}$ appear was surprising. Given that it's an olympiad problem, it suggests that there is a nice solution, which led to the guess of $(1)$.