calc
  (1 : ℤ) * 0 ≃ _ := AA.absorbR
  0           ≃ _ := Rel.symm AA.absorbR
  0 * 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
⊢ 1 * 0 ≃ 0 * 0
no goals