have : pn * rd ≃ rn * pd :=
  Integer.mul_cancelR ‹qd ≄ 0› ‹(pn * rd) * qd ≃ (rn * pd) * qd›
ℕ : 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
ℕ : 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
this : pn * rd ≃ rn * pd
⊢ pn//pd ≃ rn//rd