The following theorem appears (unproven) in Rudin's RCA:
If $\{a_n\}$ converges, then evidently $\displaystyle \limsup_{n \to \infty} a_n = \liminf_{n \to \infty} a_n = \lim_{n \to \infty} a_n $
Note that $\displaystyle \limsup_{n \to \infty} = \inf \bigg\{ \sup \{a_k \mid k \ge n \} \mid n \in \Bbb{N} \bigg\}$, and since $\displaystyle \liminf_{n \to \infty} a_n = - \limsup_{n \to \infty} (-a_n)$, we need only prove the one equality. Since $\sup \{a_k \mid k \ge n \}$ is a decreasing sequence, if it converges its limit is $\inf \bigg\{ \sup \{a_k \mid k \ge n \} \mid n \in \Bbb{N} \bigg\}$, and so the goal is to show that $\sup \{a_k \mid k \ge n \}$ converges to $\ell = \lim_{n \to \infty} a_n$ to prove that $\displaystyle \limsup_{n \to \infty} a_n = \lim_{n \to \infty} a_n$. Observe that
$$|\sup \{a_k \mid k \ge n \} - \ell| \le |\sup \{a_k \mid k \ge n \} - a_n| + |a_n - \ell|,$$
so I just need to prove that $|\sup \{a_k \mid k \ge n \} - a_n| \to 0$ as $n \to \infty$, which I am having trouble doing...
I am also wondering whether $\displaystyle \lim_{n \to \infty} a_n \le \limsup_{n \to \infty} a_n$ holds whether $a_n$ converges (either to a finite or infinte value) or diverges. Obviously once the above theorem is proven, then if $x_n$ converges, the inequality holds (in fact, equality to be precise). But I am not sure about the case when $x_n$ doesn't converge to a finite value.
$\sup \{a_n\}\ge a_n \ge \inf \{a_n\}$
$\limsup_\limits{n\to \infty} a_n, \limsup_\limits{n\to \infty} a_n$ is restricting ourselves to the special case when $n>N$
For example, if $a_n = \cos n$ then $\{a_n\}$ does not converge: $\limsup_\limits{n\to \infty} a_n =1$ and $\liminf_\limits{n\to \infty} a_n = -1$
If $\{a_n\}$ converges, then $n>N \implies |a_n - a| < \epsilon$ for any epsilon and $\limsup_\limits{n\to \infty} a_n = \lim_\limits{n\to \infty} a_n = \liminf_\limits{n\to \infty} a_n = a$