rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
h'm : v evr.valtn (-x) = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
no goals