ι : Type ?u.69452
α : Type u_1
β : Type ?u.69458
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hbd : d ≤ b
⊢ a * d ≤ c * b
ι : Type ?u.69452
α : Type u_1
β : Type ?u.69458
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hbd : d ≤ b
⊢ a / b ≤ c / d
rw [div_le_div_iff (hd.trans_le hbd) hd]
no goals
ι : Type ?u.69452
α : Type u_1
β : Type ?u.69458
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hbd : d ≤ b
⊢ a * d ≤ c * b
exact mul_le_mul hac hbd hd.le hc