no goals
ι : Type ?u.112188
α : Type u_1
β : Type ?u.112194
inst✝ : LinearOrderedSemifield α
a✝ b✝ c✝ d e : α
m n : ℤ
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b < c⁻¹ * a
rwa [← div_eq_inv_mul, lt_div_iff hc₀]