ι : Type ?u.152300
α : Type u_1
β : Type ?u.152306
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≤ 0
h : b ≤ a
⊢ a * (1 / c) ≤ b * (1 / c)
ι : Type ?u.152300
α : Type u_1
β : Type ?u.152306
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≤ 0
h : b ≤ a
⊢ a / c ≤ b / c
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
no goals
ι : Type ?u.152300
α : Type u_1
β : Type ?u.152306
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≤ 0
h : b ≤ a
⊢ a * (1 / c) ≤ b * (1 / c)
exact mul_le_mul_of_nonpos_right h (one_div_nonpos.2 hc)