have : (1 : ℤ) ≃ 0 := calc
  (1 : ℤ) ≃ _ := Rel.symm AA.identR
  1 * 1   ≃ _ := ‹(1 : ℤ) * 1 ≃ 1 * 0›
  1 * 0   ≃ _ := AA.absorbR
  0       ≃ _ := Rel.refl
ℕ : 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
x✝ : p ≃ r
this✝ : 1//0 ≃ 1//1
this : 1 * 1 ≃ 1 * 0
⊢ 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
x✝ : p ≃ r
this✝¹ : 1//0 ≃ 1//1
this✝ : 1 * 1 ≃ 1 * 0
this : 1 ≃ 0
⊢ False