rw (config := { occs := .pos [1] }) [← Int.mul_zero c, Int.mul_le_mul_left hc]
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ (c * (x - y) ≤ 0) = (x - y ≤ 0)
no goals