intro (_ : Nonzero pd) (_ : Nonzero qd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero (qn//qd).denominator → Nonzero (pn//pd + qn//qd).denominator
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pn//pd + qn//qd).denominator