補題
f(X) ∈ Z[X] を次数 m ≧ 1 の有理整数係数の多項式とする。
f'(X) をその導多項式とする。つまり f'(X) = df(X)/dx である。
p を有理素数とする。

ある有理整数 n ≧ 1 に対して合同方程式
f(X) ≡ 0 (mod p^n) が根 a を持ち、f'(a) が p で割れないなら、
f(X) ≡ 0 (mod p^(n+1)) は
b ≡ a (mod p^n)
となる根 b を持つ。このような b は mod p^(n+1) で一意に決まる。

証明
f(a) ≡ 0 (mod p^n) だから、f(a) は p^n で割れる。
よって f(a) = (p^n)t となる有理整数 t がある。

>>97 より x を任意の有理整数とすると、
f(a + (p^n)x) ≡ f(a) + f'(a)(p^n)x (mod p^(n+1))
である。

よって
f(a + (p^n)x) = f(a) + f'(a)(p^n)x + (p^(n+1))r
となる有理整数 r がある。

よって
f(a + (p^n)x) = (p^n)(t + f'(a)x + pr)

仮定より f'(a) ≡ 0 (mod p) でないから
x に関する一次合同方程式
t + f'(a)x ≡ 0 (mod p)
は解け、その解 x は mod p で一意に決まる。
b = a + (p^n)x とおけばよい。
証明終