simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
  ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
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) = ↑Nat.zero - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑Nat.zero - ↑(Nat.succ n)
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