Strong form of Hensel lemma (source code)

= Strong form of Hensel lemma

Let $K$ be complete for a <discrete valuation> $v$. If $f\in\mathcal O_K[X]$ and
$$
v(f(a))>2v(f'(a)),
$$
then <Newton iteration over a valued field> converges to a root $\alpha\in\mathcal O_K$ with $v(\alpha-a)>v(f'(a))$.