Theorem: Int.val_poly_of_double_root (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
a b c : ℤ
H : has_double_root a b c hp
⊢ SurjVal.v (primeEVR hp).valtn (a * double_root a b c p ^ 2 + b * double_root a b c p + c) > 0 ∧
    SurjVal.v (primeEVR hp).valtn (2 * a * double_root a b c p + b) > 0
Tactic:
sorry
State after:
no goals