ι : Type ?u.63758
α : Type u_1
β : Type ?u.63764
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
h : a < b
⊢ a * (1 / c) < b * (1 / c)
ι : Type ?u.63758
α : Type u_1
β : Type ?u.63764
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
h : a < b
⊢ a / c < b / c
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
no goals
ι : Type ?u.63758
α : Type u_1
β : Type ?u.63764
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 < c
h : a < b
⊢ a * (1 / c) < b * (1 / c)
exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc)