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