K : Type ?u.1744962
F : Type ?u.1744965
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1744977
Γ''₀ : Type ?u.1744980
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
g : (fun x => Γ₀) x
hx : ↑v x ≤ g
hy : ↑v y ≤ g
⊢ ↑v (x + -y) ≤ g
K : Type ?u.1744962
F : Type ?u.1744965
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1744977
Γ''₀ : Type ?u.1744980
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
g : (fun x => Γ₀) x
hx : ↑v x ≤ g
hy : ↑v y ≤ g
⊢ ↑v (x - y) ≤ g
rw [sub_eq_add_neg]
no goals
K : Type ?u.1744962
F : Type ?u.1744965
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1744977
Γ''₀ : Type ?u.1744980
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
g : (fun x => Γ₀) x
hx : ↑v x ≤ g
hy : ↑v y ≤ g
⊢ ↑v (x + -y) ≤ g
exact v.map_add_le hx (le_trans (le_of_eq (v.map_neg y)) hy)