simp [← h]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
nm : ℕ
h : Nat.zero * n = nm
⊢ sub_val evr nm (x ^ Nat.zero) = sub_val evr n x ^ Nat.zero
no goals