Theorem: SurjVal.v_sub_ge_min_v (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a - b)
Tactic:
rw [sub_eq_add_neg]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a + -b)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ min (v nav a) (v nav b) ≤ v nav (a + -b)
Tactic:
convert nav.v_add_ge_min_v a (-b) using 2
State after:
case h.e'_3.h.e'_4
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b = v nav (-b)

State before:
case h.e'_3.h.e'_4
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b = v nav (-b)
Tactic:
simp
State after:
no goals