rw [pow_zero]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (p ^ Nat.zero) = ↑Nat.zero
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 = ↑Nat.zero