calc
  -(pn//pd) + pn//pd ≃ _ := eqv_refl
  (-pn)//pd + pn//pd ≃ _ := add_eqv_denominators
  (-pn + pn)//pd     ≃ _ := substN AA.inverseL
  0//pd              ≃ _ := eqv_zero_iff_numerator_eqv_zero.mpr Rel.refl
  0                  ≃ _ := eqv_refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive pd)
⊢ -pn//pd + pn//pd ≃ 0
no goals