rw [←nav.v_eq_top_iff_zero, nav.v_uniformizer]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬p = 0
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬1 = ⊤