Unique valuation ring over a totally ramified layer

Let $R$ be a discrete valuation ring (a commutative domain that is a discrete valuation ring in the Mathlib sense) with fraction field $K$, and let $L$ be a finite separable extension of $K$, regarded as an $R$-algebra compatibly with $K$ (a scalar tower $R \to K \to L$). Let $n$ be a natural number with $0 < n$ and $\operatorname{finrank}_K L \le n$, let $\pi \in R$ be irreducible, let $u, v \in L$ satisfy $uv = 1$ with both $u$ and $v$ integral over $R$, and let $\varpi \in L$ satisfy $\varpi^{\,n} = \pi u$ (the image of $\pi$ under $R \to L$ times $u$). The conclusion is twofold: first, $\operatorname{finrank}_K L = n$; second, there is a valuation subring $W \subseteq L$ whose elements include all images of elements of $R$, such that the image of every element of the maximal ideal of $R$ lies in the maximal ideal of $W$, $W$ is a discrete valuation ring, $\varpi \in W$ and the maximal ideal of $W$ is the principal ideal generated by $\varpi$, every $w \in W$ is congruent modulo the maximal ideal of $W$ to the image of some element of $R$, an element $k \in K$ has its image in $W$ precisely when $k$ lies in the image of $R$, and any valuation subring $W'$ of $L$ containing the image of $R$ and carrying the maximal ideal of $R$ into its own maximal ideal equals $W$.

This is the statement that a layer generated by an $n$-th root of a uniformiser, up to a unit of the integral closure, is totally ramified of degree exactly $n$ over $R$, with a unique valuation ring of $L$ lying over the valuation ring $R$, residue field unchanged and $\varpi$ as uniformiser. It is used in the analysis of valuation subrings of function fields, in particular to identify the constants subring in a tower and to compare valuation subrings attached to the ends of an annulus.