intro (_ : pn//pd ≃ qn//qd) (_ : qn//qd ≃ rn//rd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd ∨ (qn//qd).to_prod ≃ (0//0).to_prod
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd ∨ (qn//qd).to_prod ≃ (0//0).to_prod