a b : Int
ha : 0 < a
hb : b < 0
h : a * b < a * 0
⊢ a * b < 0
a b : Int
ha : 0 < a
hb : b < 0
⊢ a * b < 0
have h : a * b < a * 0 := Int.mul_lt_mul_of_pos_left hb ha
no goals
a b : Int
ha : 0 < a
hb : b < 0
h : a * b < a * 0
⊢ a * b < 0
rwa [Int.mul_zero] at h