rw [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero _ _ b₁, ← this hc₁, ← this hc₂, h]
α : Type u_1
inst✝ : LinearOrderedRing α
c₁ c₂ a₁ a₂ b₁ b₂ : α
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : α}, c > 0 → (c * (x - y) ≥ 0) = (x - y ≥ 0)
⊢ (a₁ ≥ a₂) = (b₁ ≥ b₂)
no goals