apply le_antisymm
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 + 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)