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