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