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