ι : Type ?u.61284
α : Type u_1
β : Type ?u.61290
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
h : a ≤ b
⊢ a * (1 / c) ≤ b * (1 / c)
ι : Type ?u.61284
α : Type u_1
β : Type ?u.61290
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
h : a ≤ b
⊢ a / c ≤ b / c
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
no goals
ι : Type ?u.61284
α : Type u_1
β : Type ?u.61290
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
h : a ≤ b
⊢ a * (1 / c) ≤ b * (1 / c)
exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 hc)