intro (qn//qd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, pn//pd ≃ q → q ≃ r → pn//pd ≃ r ∨ q.to_prod ≃ (0//0).to_prod
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r ∨ (qn//qd).to_prod ≃ (0//0).to_prod