rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h]
a b c d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : Int}, c > 0 → (c * (x - y) > 0) = (x - y > 0)
⊢ (a₁ > a₂) = (b₁ > b₂)
no goals