**Update.** Based on Anthony Quas' comment below, the proof can be made sensibly shorter and the lemma can be slightly generalized by weakening the old assumption (iii).

In a joint paper that I am writing, we need (and prove) the following:

> **Lemma.** Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be sequences of positive real numbers such that: 
<br> <br> &nbsp;&nbsp; (i) $a_n + 1 \le b_n < a_{n+1}$ for all $n \in \mathbf{N}^+$; </br> 
<br> &nbsp;&nbsp; (ii) $a_n/b_n \to \ell$ as $n \to \infty$; </br> </br>
<br> &nbsp;&nbsp; (iii) $b_n/a_{n+1} \to 0$ as $n \to \infty$. </br>
<br> <br> Then $\mathsf{d}^\ast(X) = 1-\ell$, where $X := \bigcup_{n \ge 1} [\![ a_n+1, b_n
    ]\!]$. </br> </br>

Here, for a set $X \subseteq \mathbf{Z}$ we let $\mathsf{d}^\ast(X)$ be the upper asymptotic density of $X$, viz. 
$$\mathsf{d}^\ast(X) := \limsup_{n \to \infty} \frac{|X \cap [\![ 1, n ]\!]|}{n},$$ 
and for $a,b \in \mathbf{R}$ we set $[\![a,b]\!] := [a,b] \cap \mathbf Z$.

The proof is rather straightforward, but at the same time it takes about half a page to word it in a reasonable amount of details (EDIT: this is no longer the case). Yet, we would prefer to avoid it, so my question is:
> Do you know of a reference where the lemma, or a generalization of it, is proved?

E.g., we have tried to look at Halberstam and Roth's _Sequences_ (Springer-Verlag, 1989), but couldn't find anything.