have general : ∀ y : R, sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y := by
  induction m with
  | zero => simp [sub_val_x_zero]
  | succ m ih =>
    intro y
    cases @eq_zero_or_pos _ _ (evr.valtn y) with
    | inl h' => simp [sub_val_val_zero evr y _ h']
    | inr h' =>
      rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
      exact ih (evr.decr_val y)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
general : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x