intro (pn//pd)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 0 ↔ p.numerator ≃ 0
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 ↔ (pn//pd).numerator ≃ 0