no goals
ι : Type ?u.133631
α : Type u_1
β : Type ?u.133637
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]