rw [pow_zero, one_mul]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero (p ^ Nat.zero * x) = x
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero x = x