rw [val_of_one] at contradiction
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : v nav 1 > 0
⊢ False
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : 0 > 0
⊢ False