intro (a//b) (_ : AP (a//b ≄ 0))
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ (p : Fraction ℤ) [inst : AP (p ≄ 0)], Integer.Nonzero p.numerator
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
⊢ Integer.Nonzero (a//b).numerator