calc
  1 * pn//pd         ≃ _ := eqv_refl
  1//1 * pn//pd      ≃ _ := eqv_refl
  (1 * pn)//(1 * pd) ≃ _ := substN AA.identL
  pn//(1 * pd)       ≃ _ := substD AA.identL
  pn//pd             ≃ _ := eqv_refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ 1 * pn//pd ≃ pn//pd
no goals