no goals
ι : Type ?u.148913
α : Type u_1
β : Type ?u.148919
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : b ≤ a
hb : b ≤ 0
⊢ a / b ≤ 1
simpa only [neg_div_neg_eq] using div_le_one_of_le (neg_le_neg h) (neg_nonneg_of_nonpos hb)