have : qn * pd ≃ 0 := calc
  qn * pd ≃ _ := Rel.symm ‹pn * qd ≃ qn * pd›
  pn * qd ≃ _ := AA.substR ‹qd ≃ 0›
  pn * 0  ≃ _ := AA.absorbR
  0       ≃ _ := Rel.refl
ℕ : 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 * qd ≃ qn * pd
this : qn * rd ≃ rn * qd
⊢ 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 * qd ≃ qn * pd
this✝ : qn * rd ≃ rn * qd
this : qn * pd ≃ 0
⊢ pn * rd ≃ rn * pd ∨ (qn, qd) ≃ (0, 0)