[proofplan]
We work with the explicit Lubin--Tate polynomial $e(X) = X^q + \pi X$ and its iterates $f_n = e^{\circ n}$. The division points $F(n) = \{x \in \bar{\mathfrak{m}} : f_n(x) = 0\}$ form the root set of a polynomial of degree $q^n$ with no repeated roots (by the [No Repeated Roots for Iterated Lubin--Tate Series](/theorems/???)), so $|F(n)| = q^n$. To prove freeness of rank $1$ over $\mathcal{O}_K/\pi^n\mathcal{O}_K$, we exhibit a generator: any $\lambda_n \in F(n) \setminus F(n-1)$. We show the $\mathcal{O}_K$-module map $a \mapsto [a]_F(\lambda_n)$ has kernel exactly $\pi^n\mathcal{O}_K$ and is surjective by a cardinality argument.
[/proofplan]
[step:Identify $F(n)$ as the root set of $f_n$ and establish $|F(n)| = q^n$]
Since all Lubin--Tate formal $\mathcal{O}_K$-modules for the uniformizer $\pi$ are isomorphic (by the [classification of Lubin--Tate modules](/theorems/???)), we may compute with the explicit choice $e(X) = X^q + \pi X$, defining $F = F_e$. The endomorphism $[\pi]_F$ equals $e(X)$ by construction, so
\begin{align*}
[\pi^n]_F = \underbrace{e \circ e \circ \cdots \circ e}_{n \text{ times}} = f_n.
\end{align*}
Therefore $F(n) = \ker([\pi^n]_F) = \{x \in \bar{\mathfrak{m}} : f_n(x) = 0\}$.
The polynomial $f_n(X)$ has degree $q^n$: since $\deg(e) = q$ and $f_n = e^{\circ n}$, we have $\deg(f_n) = q^n$ (the degree of a composition is the product of degrees). By the [No Repeated Roots for Iterated Lubin--Tate Series](/theorems/???), $f_n$ has no repeated roots. A polynomial of degree $d$ over a field has at most $d$ roots, and a separable polynomial of degree $d$ over an algebraically closed field has exactly $d$ roots. Since the roots of $f_n$ lie in $\bar{K}$ (which is algebraically closed), $f_n$ has exactly $q^n$ distinct roots. Therefore $|F(n)| = q^n$.
[/step]
[step:Show that $F(n)$ is annihilated by $\pi^n$ and define the module map]
For any $x \in F(n)$, we have $[\pi^n]_F(x) = f_n(x) = 0$ by definition. Since the $\mathcal{O}_K$-action on $\bar{\mathfrak{m}}_F$ is given by $a \cdot x = [a]_F(x)$ (by the [Formal Module Action on the Maximal Ideal](/theorems/???)), this means $\pi^n \cdot x = 0$ for all $x \in F(n)$. Therefore $F(n)$ is annihilated by $\pi^n \mathcal{O}_K$ and becomes an $\mathcal{O}_K/\pi^n\mathcal{O}_K$-module.
Fix $\lambda_n \in F(n) \setminus F(n-1)$ (such an element exists since $|F(n)| = q^n > q^{n-1} = |F(n-1)|$ for $n \geq 1$). Define the $\mathcal{O}_K$-module homomorphism
\begin{align*}
\varphi \colon \mathcal{O}_K &\to F(n) \\
a &\mapsto [a]_F(\lambda_n).
\end{align*}
This is an $\mathcal{O}_K$-module map because $[a + b]_F = F([a]_F, [b]_F)$ (which is $+_F$ on the images) and $[ab]_F = [a]_F \circ [b]_F$.
[/step]
[step:Determine the kernel of $\varphi$ is $\pi^n \mathcal{O}_K$]
Since $[\pi^n]_F(\lambda_n) = f_n(\lambda_n) = 0$ (as $\lambda_n \in F(n)$), we have $\pi^n \mathcal{O}_K \subset \ker(\varphi)$.
For the reverse inclusion, suppose $a \in \ker(\varphi)$, so $[a]_F(\lambda_n) = 0$, meaning $\lambda_n \in \ker([a]_F)$. Write $a = u\pi^k$ with $u \in \mathcal{O}_K^\times$ and $k = v_K(a) \geq 0$ (if $a = 0$, then $a \in \pi^n\mathcal{O}_K$ and we are done). Then
\begin{align*}
[a]_F(\lambda_n) = [u]_F([\pi^k]_F(\lambda_n)) = [u]_F(f_k(\lambda_n)).
\end{align*}
Since $[u]_F$ is an automorphism of the formal group (as $u \in \mathcal{O}_K^\times$, the series $[u]_F$ has leading coefficient $u \neq 0$ and is therefore invertible as a power series over $\mathcal{O}_K$), $[u]_F(\alpha) = 0$ implies $\alpha = 0$. Therefore $[a]_F(\lambda_n) = 0$ gives $f_k(\lambda_n) = 0$, which means $\lambda_n \in F(k)$.
By choice, $\lambda_n \notin F(n-1)$, so we must have $k \geq n$, i.e., $v_K(a) \geq n$, i.e., $a \in \pi^n \mathcal{O}_K$.
Therefore $\ker(\varphi) = \pi^n \mathcal{O}_K$, and $\varphi$ induces an injective $\mathcal{O}_K$-module homomorphism
\begin{align*}
\bar{\varphi} \colon \mathcal{O}_K/\pi^n\mathcal{O}_K &\hookrightarrow F(n).
\end{align*}
[guided]
The key step is showing that $\lambda_n$ cannot be killed by $[\pi^k]_F$ for $k < n$. The logic is: $[a]_F = [u]_F \circ [\pi^k]_F$ where $u$ is a unit. Since $[u]_F$ is invertible (it is an automorphism of the formal module because $u \in \mathcal{O}_K^\times$), the equation $[a]_F(\lambda_n) = 0$ reduces to $[\pi^k]_F(\lambda_n) = 0$, i.e., $\lambda_n \in F(k) = \ker([\pi^k]_F)$.
Why is $[u]_F$ invertible? For a unit $u \in \mathcal{O}_K^\times$, the power series $[u]_F(X) = uX + (\text{higher order})$ has nonzero leading coefficient, so by the formal inverse function theorem for power series over a complete local ring, it has a compositional inverse. Alternatively, $[u^{-1}]_F$ is the inverse since $[u]_F \circ [u^{-1}]_F = [u \cdot u^{-1}]_F = [1]_F = \operatorname{id}$.
Now $\lambda_n \in F(n) \setminus F(n-1)$ by choice, so $\lambda_n \notin F(k)$ for any $k \leq n - 1$. This forces $k \geq n$, hence $a \in \pi^n\mathcal{O}_K$. The contrapositive: if $v_K(a) < n$, then $\lambda_n \in F(v_K(a)) \subset F(n-1)$, contradicting $\lambda_n \notin F(n-1)$.
[/guided]
[/step]
[step:Conclude by a cardinality argument that $\bar{\varphi}$ is an isomorphism]
The quotient $\mathcal{O}_K/\pi^n\mathcal{O}_K$ has cardinality $|\kappa_K|^n = q^n$: the residue field $\kappa_K = \mathcal{O}_K/\pi\mathcal{O}_K$ has $q$ elements, and $\mathcal{O}_K/\pi^n\mathcal{O}_K$ has $q^n$ elements (each coset is determined by the "digits" $a_0, a_1, \ldots, a_{n-1}$ in $a = a_0 + a_1\pi + \cdots + a_{n-1}\pi^{n-1} + \pi^n\mathcal{O}_K$ where each $a_i$ ranges over the $q$ Teichmuller representatives).
The target $F(n)$ also has cardinality $q^n$ (established in the first step). We have shown $\bar{\varphi} \colon \mathcal{O}_K/\pi^n\mathcal{O}_K \hookrightarrow F(n)$ is injective. An injective map between finite sets of the same cardinality is a bijection. Therefore $\bar{\varphi}$ is an isomorphism of $\mathcal{O}_K$-modules:
\begin{align*}
\mathcal{O}_K/\pi^n\mathcal{O}_K \xrightarrow{\;\sim\;} F(n), \qquad a + \pi^n\mathcal{O}_K \mapsto [a]_F(\lambda_n).
\end{align*}
This exhibits $F(n)$ as a free $\mathcal{O}_K/\pi^n\mathcal{O}_K$-module of rank $1$ with generator $\lambda_n = \bar{\varphi}(1 + \pi^n\mathcal{O}_K)$.
[/step]
