ι : Type ?u.152811
α : Type u_1
β : Type ?u.152817
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
h : b < a
⊢ a * (1 / c) < b * (1 / c)
ι : Type ?u.152811
α : Type u_1
β : Type ?u.152817
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.152811
α : Type u_1
β : Type ?u.152817
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
h : b < a
⊢ a * (1 / c) < b * (1 / c)
exact mul_lt_mul_of_neg_right h (one_div_neg.2 hc)