a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c * a ≤ c * b
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ a * c ≤ b * c
rw [Int.mul_comm, Int.mul_comm b]
no goals
a b c : Int
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c * a ≤ c * b
exact Int.mul_le_mul_of_nonneg_left h₁ h₂