no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
ha : Polynomial.eval a F = 0
⊢ ‖a - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
simp [deriv_ne_zero hnorm]