have : q ≃ r := by
  show 0//0 ≃ 1//1
  show 0 * 1 ≃ 1 * 0
  exact AA.comm
ℕ : 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
⊢ 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
⊢ False