How to calculate sum, if the recurrence is given? Let  $a_n=4a_{n-1}-a_{n-2}$, for $n\geq 3$. Prove that $\sum\limits_{n=1}^\infty \cot^{-1}{a_n^2}=\frac{\pi}{12}$, if $a_1=2$, $a_2=8$.
This recurrent formula is easy to solve. Characteristic equation $x^2-4x+1=0$ has two roots, $2\pm \sqrt{3}$. Therefore general solution is $a_n=a(2+\sqrt{3})^n+b(2-\sqrt{3})^n$, where a and b can be obtained from $a_1=2$ and $a_2=8$. But, I have no idea what to do next. How to calculate sum $\sum\limits_{n=1}^\infty \cot^{-1}{a_n^2}$?
Any help is welcome. Thanks in advance.
 A: Note: This is one part of a solution, the other part is in cineel's answer.
The first elements of the sequence are
$$
 a_n = 2, 8, 30, 112, 418, 1560, 5822, 21728, 81090, \ldots
$$
Using the identity
$$
\cot^{-1}(x) + \cot^{-1}(y) = \cot^{-1} \left( \frac{xy-1}{x+y}\right)
$$
we compute the first few partial sums:
$$
\begin{align}
 \sum_{k=1}^2 \cot^{-1}(a_k^2)  &= \cot^{-1}(2^2)+\cot^{-1}(8^2) = \cot^{-1}\left( \frac{4 \cdot 64 -1}{4+64}\right)
 = \cot^{-1}\left( \frac{15}{4}\right) \\
\sum_{k=1}^3 \cot^{-1}(a_k^2) &= \cot^{-1}\left( \frac{15}{4}\right)
+ \cot^{-1}(30^2) = \cot^{-1}\left( \frac{56}{15}\right)  \\
\sum_{k=1}^4 \cot^{-1}(a_k^2) &= \cot^{-1}\left( \frac{56}{15}\right)
+ \cot^{-1}(112^2) = \cot^{-1}\left( \frac{209}{56}\right)  \\
\sum_{k=1}^5 \cot^{-1}(a_k^2) &= \cot^{-1}\left( \frac{209}{56}\right)
+ \cot^{-1}(418^2) = \cot^{-1}\left( \frac{780}{209}\right) 
\end{align}
$$
Now the arguments of $\cot^{-1}$ on the right happen to be ratios of consecutive $a_n$:
$15/4 = a_3/a_2$, $56/15 = a_4/a_3$, $209/56 = a_5/a_4$, etc. This leads to the following

Conjecture: $$\sum_{k=1}^n \cot^{-1}(a_k^2)= \cot^{-1}\left( \frac{a_{n+1}}{a_n}\right) $$

If that were true then the sum of the infinite series can be computed as
$$
 \sum_{k=1}^\infty \cot^{-1}(a_k^2) = \lim_{n \to \infty} \cot^{-1}\left( \frac{a_{n+1}}{a_n}\right) = \cot^{-1}(2 + \sqrt 3) = \frac{\pi}{12} \, .
$$
and we are done. So it remains to prove the conjecture.
The formula is true for $n=1$. In order to prove it via induction, we have to show that
$$
 \frac{\frac{a_{n+1}}{a_n} a_{n+1}^2-1}{\frac{a_{n+1}}{a_n} + a_{n+1}^2}
= \frac{a_{n+2}}{a_{n+1}}
$$
holds for all $n$, or equivalently,
$$ \tag{$*$}
 \frac{a_{n+1}^3-a_n}{1+a_n a_{n+1}} = a_{n+2} \, .
$$
I have verified $(*)$ with PARI/GP for all $n \le 30$, so I am fairly sure that it is correct. However, I haven't been able yet to prove it from the recursion formula for the $a_n$.
Addendum: $(*)$ has been proved in  cineel's answer.
A: Lemma: $\frac{a_{n+1}^2+a_n^2}{1+a_na_{n+1}}=4$
solving the recurrence,
$a_n=\frac{1}{\sqrt{3}}(a^n-1/a^n)$ where $a=2+\sqrt{3}$
$a_{n+1}^2+a_n^2=\frac{1+a^2}{a}(a^{2n+1}+1/a^{2n+1})-4 =4(a^{2n+1}+1/a^{2n+1}-1)$
$1+a_n a_{n+1}=3+(a^{2n+1}+1/a^{2n+1})-(a+1/a)=a^{2n+1}+1/a^{2n+1}-1$
using the lemma,
$\frac{a_{n+1}^2+a_n^2}{1+a_na_{n+1}}=4=\frac{a_{n+2}+a_n}{a_{n+1}}$
$a_{n+2}+a_n=\frac{a_{n+1}^3+a_n^2 a_{n+1}}{1+a_na_{n+1}}$
$a_{n+2}=\frac{a_{n+1}^3-a_n}{1+a_na_{n+1}}$
then continue with Martin R's soln.
