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