have : (1 : ℤ) ≃ 0 := calc
  1     ≃ _ := Rel.symm ‹Sqrt1 a›.elim
  a * a ≃ _ := AA.substL ‹a ≃ 0›
  0 * a ≃ _ := AA.absorbL
  0     ≃ _ := Rel.refl
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ False
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
this : 1 ≃ 0
⊢ False