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: (i) $a_n + 1 \le b_n < a_{n+1}$ for all $n \in \mathbf{N}^+$; (ii) $a_n/b_n \to \ell$, for some $\ell \in \mathbf{R}$, as $n \to \infty$; (iii) $b_n/a_{n+1} \to 0$ and $n b_n/b_{n+1} \to 0$ as $n \to \infty$. Then $\mathsf{d}^\ast(X) = 1-\ell$, where $X := \bigcup_{n \ge 1} [\![ a_n+1, b_n ]\!]$.

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, to some extent, rather straightforward, but at the same time it takes about half a page to word it in a reasonable amount of details. Yet, we would prefer to avoid it, so my question is:

Does any of you here around 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.