rw [sub_eq_add_neg]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a - b)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a + -b)