Solution (source code)

= Solution

An <asymptotic sequence> satisfies
$$
\phi_{n+1}(x)=o(\phi_n(x))
\qquad(x\to x_0).
$$
The expansion
$f\sim\sum_{n\geq0}a_n\phi_n$ means that for every $N\geq0$,
$$
f(x)-\sum_{n=0}^Na_n\phi_n(x)=o(\phi_N(x)).
$$
For $N=0$, division by $\phi_0$ gives
$$
a_0=\lim_{x\to x_0}\frac f{\phi_0}.
$$
For $n\geq1$, the definition with $N=n$ says
$$
f-\sum_{k=0}^{n-1}a_k\phi_k
=a_n\phi_n+o(\phi_n).
$$
Division by $\phi_n$ gives the second coefficient formula. In particular, asymptotic-expansion coefficients are unique.