rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
decr_val_neg, sub_val_decr_val_comm]
case succ.inr
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' : 0 < v evr.valtn x
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
no goals