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
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖z' - z‖ = ‖z1‖
simp only [sub_eq_add_neg, add_assoc, hz', add_add_neg_cancel'_right, norm_neg]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖
gcongr
no goals
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
apply hz.2