∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} {a₁ b₁ : α}
  {a₂ b₂ : ↥s} {c₁ d₁ : α} {c₂ d₂ : ↥s},
  (Localization.r s) (a₁, a₂) (b₁, b₂) →
    (Localization.r s) (c₁, c₂) (d₁, d₂) → (↑c₂ * a₁ < ↑a₂ * c₁) = (↑d₂ * b₁ < ↑b₂ * d₁)