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