convert nav.v_add_ge_min_v (a + b) (-b)
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ min (v nav (a + b)) (v nav (-b)) ≤ v nav a
case h.e'_4.h.e'_6
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ a = a + b + -b