Completeness of the unit filtration attached to a shrinking chain of additive subgroups

Let $L$ be a complete normed field and let $M \colon \mathbb{N} \to$ (additive subgroups of $L$) be a family such that each $M_n$ is closed as a subset of $L$; the family is antitone, so $M_m \subseteq M_n$ whenever $n \le m$; $x \cdot y \in M_n$ whenever $x \in M_n$ and $y \in M_0$; every $x \in M_0$ has $\|x\| < 1$; and for every $\varepsilon > 0$ there is an $n$ with $\|x\| < \varepsilon$ for all $x \in M_n$. Let $(s_n)_{n \in \mathbb{N}}$ be a sequence of units of $L$ such that for every $n$ both $s_{n+1}/s_n - 1$ and $s_n/s_{n+1} - 1$ (the quotients taken in $L^\times$ and then viewed in $L$) lie in $M_n$. The conclusion is that there exists a unit $x \in L^\times$ such that for every $n$ both $x/s_n - 1 \in M_n$ and $s_n/x - 1 \in M_n$.

This is the statement that the filtration of $L^\times$ by the subgroups $\{u : u - 1 \in M_n,\ u^{-1} - 1 \in M_n\}$ is complete: a sequence of units whose consecutive ratios converge to $1$ along the filtration has a limit in the same sense. It is used in the successive-approximation construction of a unit-valued cocycle, namely by ExtCitation.LocalLevel.exists_subgroup_units_forall_isMulCocycle.