simp at h
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0
⊢ b * a < 0