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