ι : Type ?u.106331
α : Type u_1
β : Type ?u.106337
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
ι : Type ?u.106331
α : Type u_1
β : Type ?u.106337
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
rw [← mul_div_assoc] at h
no goals
ι : Type ?u.106331
α : Type u_1
β : Type ?u.106337
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
rwa [mul_comm b, ← div_le_iff hc]