apply Iff.intro
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 ↔ (pn//pd).numerator ≃ 0
case mp
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0

case mpr
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0