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_le_mul_of_nonneg_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