no goals
K : Type u_1
F : Type ?u.2467266
R : Type ?u.2467269
inst✝³ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.2467278
Γ''₀ : Type ?u.2467281
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x✝ y z : R
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ 1 < ↑v x ↔ ↑v x⁻¹ < 1
simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm