revert q
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator