calc
  (pn//pd + qn//qd) + rn//rd
    ≃ _ := eqv_refl
  (pn * qd + pd * qn)//(pd * qd) + rn//rd
    ≃ _ := eqv_refl
  ((pn * qd + pd * qn) * rd + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL AA.distribR)
  (((pn * qd) * rd + (pd * qn) * rd) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL (AA.substL AA.assoc))
  ((pn * (qd * rd) + (pd * qn) * rd) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL (AA.substR AA.assoc))
  ((pn * (qd * rd) + pd * (qn * rd)) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substR AA.assoc)
  ((pn * (qd * rd) + pd * (qn * rd)) + pd * (qd * rn))//((pd * qd) * rd)
    ≃ _ := substN AA.assoc
  (pn * (qd * rd) + (pd * (qn * rd) + pd * (qd * rn)))//((pd * qd) * rd)
    ≃ _ := substN (AA.substR (Rel.symm AA.distribL))
  (pn * (qd * rd) + pd * (qn * rd + qd * rn))//((pd * qd) * rd)
    ≃ _ := substD AA.assoc
  (pn * (qd * rd) + pd * (qn * rd + qd * rn))//(pd * (qd * rd))
    ≃ _ := eqv_refl
  pn//pd + (qn * rd + qd * rn)//(qd * rd)
    ≃ _ := eqv_refl
  pn//pd + (qn//qd + rn//rd)
    ≃ _ := eqv_refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : Logic.AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : Logic.AP (Positive rd)
⊢ pn//pd + qn//qd + rn//rd ≃ pn//pd + (qn//qd + rn//rd)
no goals