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