rw [sub_val_val_zero evr x n.succ h]
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = 0
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn x = 0