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