have x_pos_val : evr.valtn x > 0 := by
  rw [h]
  exact NeZero.pos _
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
x_pos_val : v evr.valtn x > 0
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1