α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ -↑n < x
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x
rw [Int.cast_neg]
no goals
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ -↑n < x
exact neg_lt.1 h