. apply le_of_not_lt
  intro h'
  have hm : nav a < nav (-b) := by rwa [val_neg]
  apply lt_irrefl (nav a)
  apply lt_of_lt_of_le (lt_min h' hm)
  convert nav.v_add_ge_min_v (a + b) (-b)
  simp
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)