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