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