a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * (b - a)
⊢ c * a < c * b
a b c : Int
h₁ : a < b
h₂ : 0 < c
⊢ c * a < c * b
have : 0 < c * (b - a) := Int.mul_pos h₂ (Int.sub_pos_of_lt h₁)
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * b - c * a
⊢ c * a < c * b
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * (b - a)
⊢ c * a < c * b
rw [Int.mul_sub] at this
no goals
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < c * b - c * a
⊢ c * a < c * b
exact Int.lt_of_sub_pos this