This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup: http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
Hensel's lemma gives a simple condition for the existence of a root of a polynomial.
The proof and motivation are described in the paper [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019].
p-adic, p adic, padic, p-adic integer
T is an auxiliary value that is used to control the behavior of the polynomial F.
We will construct a sequence of elements of ℤ_p satisfying successive values of ih.
Given z : ℤ_[p] satisfying ih n z, construct z' : ℤ_[p] satisfying ih (n+1) z'. We need the hypothesis ih n z, since otherwise z' is not necessarily an integer.