have : p ≄ r := by
  intro (_ : p ≃ r)
  show False
  have : (1 : ℤ)//0 ≃ 1//1 := ‹p ≃ r›
  have : (1 : ℤ) * 1 ≃ 1 * 0 := ‹(1 : ℤ)//0 ≃ 1//1›
  have : (1 : ℤ) ≃ 0 := calc
    (1 : ℤ) ≃ _ := Rel.symm AA.identR
    1 * 1   ≃ _ := ‹(1 : ℤ) * 1 ≃ 1 * 0›
    1 * 0   ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : (1 : ℤ) ≄ 0 := Integer.one_neqv_zero
  exact absurd ‹(1 : ℤ) ≃ 0› ‹(1 : ℤ) ≄ 0›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ False
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
this : p ≄ r
⊢ False