rw [←neg_neg 1, ←one_mul 1, neg_mul_eq_neg_mul, neg_mul_eq_mul_neg, nav.v_mul_eq_add_v]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav 1 > 0
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav (-1) + v nav (-1) > 0