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

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