rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr m (decr_val evr y)) = sub_val evr (m + n) (decr_val evr y)