have : (pn * rd) * qd ≃ (rn * pd) * qd := calc
  (pn * rd) * qd ≃ _ := AA.substL AA.comm
  (rd * pn) * qd ≃ _ := AA.assoc
  rd * (pn * qd) ≃ _ := AA.substR ‹pn * qd ≃ qn * pd›
  rd * (qn * pd) ≃ _ := Rel.symm AA.assoc
  (rd * qn) * pd ≃ _ := AA.substL AA.comm
  (qn * rd) * pd ≃ _ := AA.substL ‹qn * rd ≃ rn * qd›
  (rn * qd) * pd ≃ _ := AA.assoc
  rn * (qd * pd) ≃ _ := AA.substR AA.comm
  rn * (pd * qd) ≃ _ := Rel.symm AA.assoc
  (rn * pd) * qd ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : pn * rd * qd ≃ rn * pd * qd
⊢ pn//pd ≃ rn//rd