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