F : Type ?u.27406
ι : Type ?u.27409
α : Type u_1
β : Type ?u.27415
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ a ≤ -1
F : Type ?u.27406
ι : Type ?u.27409
α : Type u_1
β : Type ?u.27415
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ ↑a ≤ -1
rw [← Int.cast_one, ← Int.cast_neg, cast_le]
no goals
F : Type ?u.27406
ι : Type ?u.27409
α : Type u_1
β : Type ?u.27415
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ a ≤ -1
exact Int.le_sub_one_of_lt h