dsimp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ (fun x => x + v nav p) (v nav 1) = (fun x => x + v nav p) 0
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 + v nav p = 0 + v nav p