simpa [sub_val_x_zero]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m
⊢ v evr.valtn (sub_val evr Nat.zero x) = ↑m - ↑Nat.zero
no goals