calc
  (0 : ℤ)//1 + pn//pd         ≃ _ := eqv_refl
  (0 * pd + 1 * pn)//(1 * pd) ≃ _ := substN (AA.substL AA.absorbL)
  (0 + 1 * pn)//(1 * pd)      ≃ _ := substN AA.identL
  (1 * pn)//(1 * pd)          ≃ _ := substN AA.identL
  pn//(1 * pd)                ≃ _ := substD AA.identL
  pn//pd                      ≃ _ := eqv_refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0//1 + pn//pd ≃ pn//pd
no goals