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