no goals
ι : Type ?u.73311
α : Type u_1
β : Type ?u.73317
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 1 < b
⊢ a / b < a
simpa only [div_one] using div_lt_div_of_lt_left ha zero_lt_one hb