ι : Type ?u.11809
α : Type u_1
β : Type ?u.11815
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0
ι : Type ?u.11809
α : Type u_1
β : Type ?u.11815
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a / b ≤ 0
rw [div_eq_mul_inv]
no goals
ι : Type ?u.11809
α : Type u_1
β : Type ?u.11815
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0
exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)