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:

   (i) $a_n + 1 \le b_n < a_{n+1}$ for all $n \in \mathbf{N}^+$;
   (ii) $a_n/b_n \to \ell$ as $n \to \infty$;
   (iii) $b_n/a_{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 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.