. exact le_trans (le_min (le_of_eq rfl) (le_of_lt h)) (SurjVal.v_add_ge_min_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)
no goals