calc
  _ ≃ sgn (p * r - q * r) := Rel.refl
  _ ≃ sgn (r * p - q * r) := sgn_subst (sub_substL mul_comm)
  _ ≃ sgn (r * p - r * q) := sgn_subst (sub_substR mul_comm)
  _ ≃ sgn (p - q)         := sgn_sub_cancelL_mul_pos ‹sgn r ≃ 1›
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q r : ℚ
x✝ : sgn r ≃ 1
⊢ sgn (p * r - q * r) ≃ sgn (p - q)
no goals