have h := mul_lt_mul_of_pos_left h₁ h₂
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
⊢ b * a < 0
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a < 0
h₂ : b > 0
h : b * a < b * 0
⊢ b * a < 0