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