have : pn//pd ≃ 1//1 := ‹pn//pd ≃ 1//1›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
⊢ pn ≃ pd
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
this : pn//pd ≃ 1//1
⊢ pn ≃ pd