K : Type ?u.2215047
F : Type ?u.2215050
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2215062
Γ''₀ : Type ?u.2215065
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v y < ↑v x
⊢ ↑v (y + x) = ↑v x
K : Type ?u.2215047
F : Type ?u.2215050
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2215062
Γ''₀ : Type ?u.2215065
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v y < ↑v x
⊢ ↑v (x + y) = ↑v x
rw [add_comm]
no goals
K : Type ?u.2215047
F : Type ?u.2215050
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2215062
Γ''₀ : Type ?u.2215065
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v y < ↑v x
⊢ ↑v (y + x) = ↑v x
exact map_add_eq_of_lt_right _ h