This aim of this question is to determine whether there exists a proof (or some counterexample) to the following statement : "If $R$ is a subring of Dedekind domain $S$, such that $S$ has a power basis as an $R$-module, then $R$ is itself a Dedekind domain".

The context is the following: I have recently been working on formalizing (using Lean) the Dedekind-Kummer theorem, which can be stated as follows [Proposition 8.3, *Algebraic number theory*, Neukirch] :

Let $\mathcal{O}$ be a Dedekind domain with field of fractions $K$ and $L$ a finite separable extension of $K$, and set $\mathcal{O'}$ to be the integral closure of $\mathcal{O}$ in $L$. If we pick a prime ideal $\mathfrak{p}$ of $\mathcal{O}$ and $\theta \in \mathcal{O}'$ such that the conductor ideal $\mathcal{C}$ of $\mathcal{O}[\theta]$ is coprime with $\mathfrak{p}$ and $L=K(\theta)$, then the prime factorisations of $\mathfrak{p} \mathcal{O'}$ and $\overline{f}$ have the same shape (in other words, there is a bijection between the sets of prime factors of $\mathfrak{p} \mathcal{O'}$ and $\overline{f}$ that preserves multiplicities), where $f$ is the minimal polynomial of $\theta$ over $K$ and $\overline{f}$ is the reduction mod $\mathfrak{p}$ of $f$.
****

So far the case when $\mathcal{O'} = \mathcal{O}[\theta]$ has been fully formalized, but the formalization does not use the assumption that $\mathcal{O}$ is a Dedekind domain. The aim of this question is thus to determine whether or not this is actually a generalization of the original statement (at least for this particular case).****