simp [sub_val_x_zero]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ ∀ (y : R), sub_val evr n (sub_val evr Nat.zero y) = sub_val evr (Nat.zero + n) y
no goals