case mp =>
  intro (_ : pn//pd ≃ 0)
  show pn ≃ 0
  have : pn//pd ≃ 0//1 := ‹pn//pd ≃ 0›
  have : pn * 1 ≃ 0 * pd := ‹pn//pd ≃ 0//1›
  calc
    pn     ≃ _ := Rel.symm AA.identR
    pn * 1 ≃ _ := ‹pn * 1 ≃ 0 * pd›
    0 * pd ≃ _ := AA.absorbL
    0      ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0
no goals