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