have : pn * rd ≃ rn * pd :=
  eqv_trans_nonzero_denom
    (q := qn//qd)
    ‹qd ≄ 0›
    ‹pn//pd ≃ qn//qd›
    ‹qn//qd ≃ rn//rd›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : Decidable (qd ≃ 0)
h✝ : qd ≄ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : Decidable (qd ≃ 0)
h✝ : qd ≄ 0
this : pn * rd ≃ rn * pd
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)