calc
  (-p₁n) * p₂d   ≃ _ := Rel.symm AA.scompatL
  (-(p₁n * p₂d)) ≃ _ := AA.subst₁ ‹p₁n * p₂d ≃ p₂n * p₁d›
  (-(p₂n * p₁d)) ≃ _ := AA.scompatL
  (-p₂n) * p₁d   ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
no goals