intro h'
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
⊢ ¬v nav a < v nav (a + 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)
⊢ False