rw [← v_mul_eq_add_v]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 + v nav p = 0 + v nav p
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (1 * p) = 0 + v nav p